YES 4.556 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ CR

mainModule Main
  ((minimum :: Ord a => [Maybe a ->  Maybe a) :: Ord a => [Maybe a ->  Maybe a)

module Main where
  import qualified Prelude



Case Reductions:
The following Case expression
case compare x y of
 EQ → o
 LT → LT
 GT → GT

is transformed to
primCompAux0 o EQ = o
primCompAux0 o LT = LT
primCompAux0 o GT = GT



↳ HASKELL
  ↳ CR
HASKELL
      ↳ IFR

mainModule Main
  ((minimum :: Ord a => [Maybe a ->  Maybe a) :: Ord a => [Maybe a ->  Maybe a)

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to
primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0 x y False = Zero

The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to
primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)
primModNatS0 x y False = Succ x



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
HASKELL
          ↳ BR

mainModule Main
  ((minimum :: Ord a => [Maybe a ->  Maybe a) :: Ord a => [Maybe a ->  Maybe a)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  ((minimum :: Ord a => [Maybe a ->  Maybe a) :: Ord a => [Maybe a ->  Maybe a)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
compare x y
 | x == y
 = EQ
 | x <= y
 = LT
 | otherwise
 = GT

is transformed to
compare x y = compare3 x y

compare2 x y True = EQ
compare2 x y False = compare1 x y (x <= y)

compare1 x y True = LT
compare1 x y False = compare0 x y otherwise

compare0 x y True = GT

compare3 x y = compare2 x y (x == y)

The following Function with conditions
min x y
 | x <= y
 = x
 | otherwise
 = y

is transformed to
min x y = min2 x y

min1 x y True = x
min1 x y False = min0 x y otherwise

min0 x y True = y

min2 x y = min1 x y (x <= y)

The following Function with conditions
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd' x zx = gcd'2 x zx
gcd' x y = gcd'0 x y

gcd'0 x y = gcd' y (x `rem` y)

gcd'1 True x zx = x
gcd'1 zy zz vuu = gcd'0 zz vuu

gcd'2 x zx = gcd'1 (zx == 0) x zx
gcd'2 vuv vuw = gcd'0 vuv vuw

The following Function with conditions
gcd 0 0 = error []
gcd x y = 
gcd' (abs x) (abs y)
where 
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd vux vuy = gcd3 vux vuy
gcd x y = gcd0 x y

gcd0 x y = 
gcd' (abs x) (abs y)
where 
gcd' x zx = gcd'2 x zx
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x zx = x
gcd'1 zy zz vuu = gcd'0 zz vuu
gcd'2 x zx = gcd'1 (zx == 0) x zx
gcd'2 vuv vuw = gcd'0 vuv vuw

gcd1 True vux vuy = error []
gcd1 vuz vvu vvv = gcd0 vvu vvv

gcd2 True vux vuy = gcd1 (vuy == 0) vux vuy
gcd2 vvw vvx vvy = gcd0 vvx vvy

gcd3 vux vuy = gcd2 (vux == 0) vux vuy
gcd3 vvz vwu = gcd0 vvz vwu

The following Function with conditions
absReal x
 | x >= 0
 = x
 | otherwise
 = `negate` x

is transformed to
absReal x = absReal2 x

absReal0 x True = `negate` x

absReal1 x True = x
absReal1 x False = absReal0 x otherwise

absReal2 x = absReal1 x (x >= 0)

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
reduce x y
 | y == 0
 = error []
 | otherwise
 = x `quot` d :% (y `quot` d)
where 
d  = gcd x y

is transformed to
reduce x y = reduce2 x y

reduce2 x y = 
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ LetRed

mainModule Main
  ((minimum :: Ord a => [Maybe a ->  Maybe a) :: Ord a => [Maybe a ->  Maybe a)

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise

are unpacked to the following functions on top level
reduce2D vwv vww = gcd vwv vww

reduce2Reduce1 vwv vww x y True = error []
reduce2Reduce1 vwv vww x y False = reduce2Reduce0 vwv vww x y otherwise

reduce2Reduce0 vwv vww x y True = x `quot` reduce2D vwv vww :% (y `quot` reduce2D vwv vww)

The bindings of the following Let/Where expression
gcd' (abs x) (abs y)
where 
gcd' x zx = gcd'2 x zx
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x zx = x
gcd'1 zy zz vuu = gcd'0 zz vuu
gcd'2 x zx = gcd'1 (zx == 0) x zx
gcd'2 vuv vuw = gcd'0 vuv vuw

are unpacked to the following functions on top level
gcd0Gcd'2 x zx = gcd0Gcd'1 (zx == 0) x zx
gcd0Gcd'2 vuv vuw = gcd0Gcd'0 vuv vuw

gcd0Gcd'0 x y = gcd0Gcd' y (x `rem` y)

gcd0Gcd'1 True x zx = x
gcd0Gcd'1 zy zz vuu = gcd0Gcd'0 zz vuu

gcd0Gcd' x zx = gcd0Gcd'2 x zx
gcd0Gcd' x y = gcd0Gcd'0 x y



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
HASKELL
                      ↳ NumRed

mainModule Main
  ((minimum :: Ord a => [Maybe a ->  Maybe a) :: Ord a => [Maybe a ->  Maybe a)

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule Main
  (minimum :: Ord a => [Maybe a ->  Maybe a)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(vwx30000), Succ(vwx310000)) → new_primCmpNat(vwx30000, vwx310000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vwx6500), Succ(vwx31001000)) → new_primPlusNat(vwx6500, vwx31001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vwx300000), Succ(vwx3100100)) → new_primMulNat(vwx300000, Succ(vwx3100100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(vwx2000), Succ(vwx2100)) → new_primEqNat(vwx2000, vwx2100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs1(Just(vwx200), Just(vwx210), app(app(app(ty_@3, gc), gd), ge)) → new_esEs(vwx200, vwx210, gc, gd, ge)
new_esEs3(Right(vwx200), Right(vwx210), bdb, app(app(ty_@2, bdh), bea)) → new_esEs2(vwx200, vwx210, bdh, bea)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), ba, app(ty_[], da), cg) → new_esEs0(vwx201, vwx211, da)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), ba, bb, app(ty_Maybe, bg)) → new_esEs1(vwx202, vwx212, bg)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), app(app(ty_Either, ef), eg), bb, cg) → new_esEs3(vwx200, vwx210, ef, eg)
new_esEs2(@2(vwx200, vwx201), @2(vwx210, vwx211), app(ty_[], bbb), bba) → new_esEs0(vwx200, vwx210, bbb)
new_esEs2(@2(vwx200, vwx201), @2(vwx210, vwx211), hd, app(ty_Maybe, baa)) → new_esEs1(vwx201, vwx211, baa)
new_esEs2(@2(vwx200, vwx201), @2(vwx210, vwx211), hd, app(app(ty_@2, bab), bac)) → new_esEs2(vwx201, vwx211, bab, bac)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), ba, bb, app(ty_[], bf)) → new_esEs0(vwx202, vwx212, bf)
new_esEs3(Left(vwx200), Left(vwx210), app(ty_Maybe, bce), bcc) → new_esEs1(vwx200, vwx210, bce)
new_esEs2(@2(vwx200, vwx201), @2(vwx210, vwx211), app(ty_Maybe, bbc), bba) → new_esEs1(vwx200, vwx210, bbc)
new_esEs3(Right(vwx200), Right(vwx210), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(vwx200, vwx210, beb, bec)
new_esEs2(@2(vwx200, vwx201), @2(vwx210, vwx211), app(app(ty_@2, bbd), bbe), bba) → new_esEs2(vwx200, vwx210, bbd, bbe)
new_esEs0(:(vwx200, vwx201), :(vwx210, vwx211), app(app(app(ty_@3, fa), fb), fc)) → new_esEs(vwx200, vwx210, fa, fb, fc)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), app(app(app(ty_@3, dg), dh), ea), bb, cg) → new_esEs(vwx200, vwx210, dg, dh, ea)
new_esEs2(@2(vwx200, vwx201), @2(vwx210, vwx211), hd, app(app(app(ty_@3, he), hf), hg)) → new_esEs(vwx201, vwx211, he, hf, hg)
new_esEs1(Just(vwx200), Just(vwx210), app(ty_[], gf)) → new_esEs0(vwx200, vwx210, gf)
new_esEs3(Left(vwx200), Left(vwx210), app(app(ty_Either, bch), bda), bcc) → new_esEs3(vwx200, vwx210, bch, bda)
new_esEs0(:(vwx200, vwx201), :(vwx210, vwx211), app(app(ty_Either, ga), gb)) → new_esEs3(vwx200, vwx210, ga, gb)
new_esEs1(Just(vwx200), Just(vwx210), app(app(ty_Either, hb), hc)) → new_esEs3(vwx200, vwx210, hb, hc)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), app(ty_Maybe, ec), bb, cg) → new_esEs1(vwx200, vwx210, ec)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), ba, app(ty_Maybe, db), cg) → new_esEs1(vwx201, vwx211, db)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), app(app(ty_@2, ed), ee), bb, cg) → new_esEs2(vwx200, vwx210, ed, ee)
new_esEs0(:(vwx200, vwx201), :(vwx210, vwx211), app(ty_Maybe, ff)) → new_esEs1(vwx200, vwx210, ff)
new_esEs3(Right(vwx200), Right(vwx210), bdb, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs(vwx200, vwx210, bdc, bdd, bde)
new_esEs3(Left(vwx200), Left(vwx210), app(app(ty_@2, bcf), bcg), bcc) → new_esEs2(vwx200, vwx210, bcf, bcg)
new_esEs2(@2(vwx200, vwx201), @2(vwx210, vwx211), app(app(app(ty_@3, baf), bag), bah), bba) → new_esEs(vwx200, vwx210, baf, bag, bah)
new_esEs3(Left(vwx200), Left(vwx210), app(ty_[], bcd), bcc) → new_esEs0(vwx200, vwx210, bcd)
new_esEs2(@2(vwx200, vwx201), @2(vwx210, vwx211), hd, app(app(ty_Either, bad), bae)) → new_esEs3(vwx201, vwx211, bad, bae)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), ba, app(app(ty_@2, dc), dd), cg) → new_esEs2(vwx201, vwx211, dc, dd)
new_esEs3(Right(vwx200), Right(vwx210), bdb, app(ty_[], bdf)) → new_esEs0(vwx200, vwx210, bdf)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), ba, app(app(app(ty_@3, cd), ce), cf), cg) → new_esEs(vwx201, vwx211, cd, ce, cf)
new_esEs3(Right(vwx200), Right(vwx210), bdb, app(ty_Maybe, bdg)) → new_esEs1(vwx200, vwx210, bdg)
new_esEs1(Just(vwx200), Just(vwx210), app(ty_Maybe, gg)) → new_esEs1(vwx200, vwx210, gg)
new_esEs1(Just(vwx200), Just(vwx210), app(app(ty_@2, gh), ha)) → new_esEs2(vwx200, vwx210, gh, ha)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), app(ty_[], eb), bb, cg) → new_esEs0(vwx200, vwx210, eb)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), ba, bb, app(app(ty_@2, bh), ca)) → new_esEs2(vwx202, vwx212, bh, ca)
new_esEs2(@2(vwx200, vwx201), @2(vwx210, vwx211), hd, app(ty_[], hh)) → new_esEs0(vwx201, vwx211, hh)
new_esEs0(:(vwx200, vwx201), :(vwx210, vwx211), app(ty_[], fd)) → new_esEs0(vwx200, vwx210, fd)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), ba, app(app(ty_Either, de), df), cg) → new_esEs3(vwx201, vwx211, de, df)
new_esEs2(@2(vwx200, vwx201), @2(vwx210, vwx211), app(app(ty_Either, bbf), bbg), bba) → new_esEs3(vwx200, vwx210, bbf, bbg)
new_esEs0(:(vwx200, vwx201), :(vwx210, vwx211), app(app(ty_@2, fg), fh)) → new_esEs2(vwx200, vwx210, fg, fh)
new_esEs3(Left(vwx200), Left(vwx210), app(app(app(ty_@3, bbh), bca), bcb), bcc) → new_esEs(vwx200, vwx210, bbh, bca, bcb)
new_esEs0(:(vwx200, vwx201), :(vwx210, vwx211), eh) → new_esEs0(vwx201, vwx211, eh)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), ba, bb, app(app(ty_Either, cb), cc)) → new_esEs3(vwx202, vwx212, cb, cc)
new_esEs(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), ba, bb, app(app(app(ty_@3, bc), bd), be)) → new_esEs(vwx202, vwx212, bc, bd, be)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_compare(:(vwx3000, vwx3001), :(vwx31000, vwx31001), baf) → new_primCompAux(vwx3000, vwx31000, new_compare4(vwx3001, vwx31001, baf), baf)
new_ltEs0(Just(vwx3000), Just(vwx31000), app(app(app(ty_@3, ea), eb), ec)) → new_ltEs1(vwx3000, vwx31000, ea, eb, ec)
new_lt(vwx3000, vwx31000, eg, eh) → new_compare2(vwx3000, vwx31000, new_esEs4(vwx3000, vwx31000, eg, eh), eg, eh)
new_primCompAux(vwx3000, vwx31000, vwx47, app(app(ty_@2, bbf), bbg)) → new_compare5(vwx3000, vwx31000, bbf, bbg)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, app(ty_[], hb), fb) → new_lt2(vwx3001, vwx31001, hb)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, app(app(app(ty_@3, gg), gh), ha), fb) → new_lt1(vwx3001, vwx31001, gg, gh, ha)
new_compare22(vwx3000, vwx31000, False, ga, gb) → new_ltEs3(vwx3000, vwx31000, ga, gb)
new_ltEs3(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), app(app(app(ty_@3, bcd), bce), bcf), bcb) → new_lt1(vwx3000, vwx31000, bcd, bce, bcf)
new_compare2(vwx3000, vwx31000, False, eg, eh) → new_ltEs(vwx3000, vwx31000, eg, eh)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, fa, app(app(ty_@2, bad), bae)) → new_ltEs3(vwx3002, vwx31002, bad, bae)
new_ltEs(Left(vwx3000), Left(vwx31000), app(app(ty_Either, ba), bb), bc) → new_ltEs(vwx3000, vwx31000, ba, bb)
new_ltEs(Right(vwx3000), Right(vwx31000), cc, app(app(ty_Either, cd), ce)) → new_ltEs(vwx3000, vwx31000, cd, ce)
new_ltEs0(Just(vwx3000), Just(vwx31000), app(app(ty_@2, ee), ef)) → new_ltEs3(vwx3000, vwx31000, ee, ef)
new_ltEs3(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), bdb, app(ty_Maybe, bde)) → new_ltEs0(vwx3001, vwx31001, bde)
new_ltEs3(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), bdb, app(app(app(ty_@3, bdf), bdg), bdh)) → new_ltEs1(vwx3001, vwx31001, bdf, bdg, bdh)
new_compare21(vwx3000, vwx31000, False, fd, ff, fg) → new_ltEs1(vwx3000, vwx31000, fd, ff, fg)
new_ltEs3(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), bdb, app(ty_[], bea)) → new_ltEs2(vwx3001, vwx31001, bea)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, app(ty_Maybe, gf), fb) → new_lt0(vwx3001, vwx31001, gf)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), app(ty_[], fh), fa, fb) → new_compare(vwx3000, vwx31000, fh)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, app(app(ty_@2, hc), hd), fb) → new_lt3(vwx3001, vwx31001, hc, hd)
new_primCompAux(vwx3000, vwx31000, vwx47, app(app(ty_Either, bag), bah)) → new_compare0(vwx3000, vwx31000, bag, bah)
new_ltEs0(Just(vwx3000), Just(vwx31000), app(ty_Maybe, dh)) → new_ltEs0(vwx3000, vwx31000, dh)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), app(app(ty_@2, ga), gb), fa, fb) → new_compare22(vwx3000, vwx31000, new_esEs7(vwx3000, vwx31000, ga, gb), ga, gb)
new_lt3(vwx3000, vwx31000, ga, gb) → new_compare22(vwx3000, vwx31000, new_esEs7(vwx3000, vwx31000, ga, gb), ga, gb)
new_primCompAux(vwx3000, vwx31000, vwx47, app(ty_[], bbe)) → new_compare(vwx3000, vwx31000, bbe)
new_ltEs(Left(vwx3000), Left(vwx31000), app(app(ty_@2, ca), cb), bc) → new_ltEs3(vwx3000, vwx31000, ca, cb)
new_ltEs(Right(vwx3000), Right(vwx31000), cc, app(app(app(ty_@3, cg), da), db)) → new_ltEs1(vwx3000, vwx31000, cg, da, db)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), app(ty_Maybe, fc), fa, fb) → new_compare20(vwx3000, vwx31000, new_esEs5(vwx3000, vwx31000, fc), fc)
new_compare1(vwx3000, vwx31000, fc) → new_compare20(vwx3000, vwx31000, new_esEs5(vwx3000, vwx31000, fc), fc)
new_ltEs3(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), bdb, app(app(ty_@2, beb), bec)) → new_ltEs3(vwx3001, vwx31001, beb, bec)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), app(app(app(ty_@3, fd), ff), fg), fa, fb) → new_compare21(vwx3000, vwx31000, new_esEs6(vwx3000, vwx31000, fd, ff, fg), fd, ff, fg)
new_ltEs3(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), app(ty_Maybe, bcc), bcb) → new_lt0(vwx3000, vwx31000, bcc)
new_ltEs(Right(vwx3000), Right(vwx31000), cc, app(app(ty_@2, dd), de)) → new_ltEs3(vwx3000, vwx31000, dd, de)
new_compare3(vwx3000, vwx31000, fd, ff, fg) → new_compare21(vwx3000, vwx31000, new_esEs6(vwx3000, vwx31000, fd, ff, fg), fd, ff, fg)
new_ltEs3(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), bdb, app(app(ty_Either, bdc), bdd)) → new_ltEs(vwx3001, vwx31001, bdc, bdd)
new_ltEs3(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), app(app(ty_@2, bch), bda), bcb) → new_lt3(vwx3000, vwx31000, bch, bda)
new_ltEs2(:(vwx3000, vwx3001), :(vwx31000, vwx31001), baf) → new_compare(vwx3001, vwx31001, baf)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, fa, app(ty_[], bac)) → new_ltEs2(vwx3002, vwx31002, bac)
new_ltEs2(:(vwx3000, vwx3001), :(vwx31000, vwx31001), baf) → new_primCompAux(vwx3000, vwx31000, new_compare4(vwx3001, vwx31001, baf), baf)
new_ltEs0(Just(vwx3000), Just(vwx31000), app(ty_[], ed)) → new_ltEs2(vwx3000, vwx31000, ed)
new_compare(:(vwx3000, vwx3001), :(vwx31000, vwx31001), baf) → new_compare(vwx3001, vwx31001, baf)
new_primCompAux(vwx3000, vwx31000, vwx47, app(ty_Maybe, bba)) → new_compare1(vwx3000, vwx31000, bba)
new_primCompAux(vwx3000, vwx31000, vwx47, app(app(app(ty_@3, bbb), bbc), bbd)) → new_compare3(vwx3000, vwx31000, bbb, bbc, bbd)
new_ltEs(Left(vwx3000), Left(vwx31000), app(ty_Maybe, bd), bc) → new_ltEs0(vwx3000, vwx31000, bd)
new_compare5(vwx3000, vwx31000, ga, gb) → new_compare22(vwx3000, vwx31000, new_esEs7(vwx3000, vwx31000, ga, gb), ga, gb)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, fa, app(app(app(ty_@3, hh), baa), bab)) → new_ltEs1(vwx3002, vwx31002, hh, baa, bab)
new_ltEs(Left(vwx3000), Left(vwx31000), app(app(app(ty_@3, be), bf), bg), bc) → new_ltEs1(vwx3000, vwx31000, be, bf, bg)
new_lt2(vwx3000, vwx31000, fh) → new_compare(vwx3000, vwx31000, fh)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, fa, app(ty_Maybe, hg)) → new_ltEs0(vwx3002, vwx31002, hg)
new_ltEs3(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), app(app(ty_Either, bbh), bca), bcb) → new_lt(vwx3000, vwx31000, bbh, bca)
new_lt1(vwx3000, vwx31000, fd, ff, fg) → new_compare21(vwx3000, vwx31000, new_esEs6(vwx3000, vwx31000, fd, ff, fg), fd, ff, fg)
new_compare0(vwx3000, vwx31000, eg, eh) → new_compare2(vwx3000, vwx31000, new_esEs4(vwx3000, vwx31000, eg, eh), eg, eh)
new_ltEs(Left(vwx3000), Left(vwx31000), app(ty_[], bh), bc) → new_ltEs2(vwx3000, vwx31000, bh)
new_ltEs(Right(vwx3000), Right(vwx31000), cc, app(ty_[], dc)) → new_ltEs2(vwx3000, vwx31000, dc)
new_ltEs(Right(vwx3000), Right(vwx31000), cc, app(ty_Maybe, cf)) → new_ltEs0(vwx3000, vwx31000, cf)
new_compare20(vwx3000, vwx31000, False, fc) → new_ltEs0(vwx3000, vwx31000, fc)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, fa, app(app(ty_Either, he), hf)) → new_ltEs(vwx3002, vwx31002, he, hf)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), app(app(ty_Either, eg), eh), fa, fb) → new_compare2(vwx3000, vwx31000, new_esEs4(vwx3000, vwx31000, eg, eh), eg, eh)
new_ltEs1(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, app(app(ty_Either, gd), ge), fb) → new_lt(vwx3001, vwx31001, gd, ge)
new_lt0(vwx3000, vwx31000, fc) → new_compare20(vwx3000, vwx31000, new_esEs5(vwx3000, vwx31000, fc), fc)
new_ltEs0(Just(vwx3000), Just(vwx31000), app(app(ty_Either, df), dg)) → new_ltEs(vwx3000, vwx31000, df, dg)
new_ltEs3(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), app(ty_[], bcg), bcb) → new_lt2(vwx3000, vwx31000, bcg)

The TRS R consists of the following rules:

new_esEs26(vwx200, vwx210, ty_Char) → new_esEs14(vwx200, vwx210)
new_esEs16(GT, EQ) → False
new_esEs16(EQ, GT) → False
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Ordering, bc) → new_ltEs14(vwx3000, vwx31000)
new_esEs20(vwx202, vwx212, ty_Ordering) → new_esEs16(vwx202, vwx212)
new_lt6(vwx3001, vwx31001, app(app(app(ty_@3, gg), gh), ha)) → new_lt10(vwx3001, vwx31001, gg, gh, ha)
new_esEs20(vwx202, vwx212, ty_Double) → new_esEs19(vwx202, vwx212)
new_compare15(vwx3000, vwx31000, True, eg, eh) → LT
new_esEs20(vwx202, vwx212, ty_@0) → new_esEs8(vwx202, vwx212)
new_ltEs14(GT, GT) → True
new_esEs27(vwx200, vwx210, app(ty_Ratio, dbf)) → new_esEs18(vwx200, vwx210, dbf)
new_esEs4(Right(vwx200), Right(vwx210), bgb, app(app(app(ty_@3, cdf), cdg), cdh)) → new_esEs6(vwx200, vwx210, cdf, cdg, cdh)
new_lt20(vwx3000, vwx31000, ty_Float) → new_lt14(vwx3000, vwx31000)
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Float, bc) → new_ltEs5(vwx3000, vwx31000)
new_ltEs6(Nothing, Just(vwx31000), bed) → True
new_ltEs7(Left(vwx3000), Left(vwx31000), app(app(ty_@2, ca), cb), bc) → new_ltEs17(vwx3000, vwx31000, ca, cb)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Char) → new_ltEs16(vwx3000, vwx31000)
new_esEs4(Right(vwx200), Right(vwx210), bgb, app(ty_Maybe, cec)) → new_esEs5(vwx200, vwx210, cec)
new_esEs4(Left(vwx200), Left(vwx210), ty_Double, bgc) → new_esEs19(vwx200, vwx210)
new_lt17(vwx3000, vwx31000) → new_esEs9(new_compare16(vwx3000, vwx31000))
new_esEs26(vwx200, vwx210, ty_Float) → new_esEs13(vwx200, vwx210)
new_ltEs7(Left(vwx3000), Right(vwx31000), cc, bc) → True
new_primMulNat0(Zero, Zero) → Zero
new_compare13(vwx3000, vwx31000, False, fd, ff, fg) → GT
new_primCompAux0(vwx3000, vwx31000, vwx47, baf) → new_primCompAux00(vwx47, new_compare32(vwx3000, vwx31000, baf))
new_sr(Integer(vwx30000), Integer(vwx310010)) → Integer(new_primMulInt(vwx30000, vwx310010))
new_lt8(vwx3000, vwx31000, fc) → new_esEs9(new_compare28(vwx3000, vwx31000, fc))
new_lt4(vwx3000, vwx31000) → new_esEs9(new_compare9(vwx3000, vwx31000))
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_@0, bc) → new_ltEs8(vwx3000, vwx31000)
new_esEs4(Right(vwx200), Right(vwx210), bgb, app(ty_Ratio, ceb)) → new_esEs18(vwx200, vwx210, ceb)
new_ltEs18(vwx3002, vwx31002, ty_Char) → new_ltEs16(vwx3002, vwx31002)
new_esEs9(LT) → True
new_esEs24(vwx200, vwx210, ty_Integer) → new_esEs15(vwx200, vwx210)
new_esEs25(vwx201, vwx211, app(ty_Ratio, cha)) → new_esEs18(vwx201, vwx211, cha)
new_lt5(vwx3000, vwx31000, app(app(ty_Either, eg), eh)) → new_lt7(vwx3000, vwx31000, eg, eh)
new_esEs4(Right(vwx200), Right(vwx210), bgb, ty_Bool) → new_esEs11(vwx200, vwx210)
new_not(GT) → False
new_esEs20(vwx202, vwx212, app(app(ty_Either, bhf), bhg)) → new_esEs4(vwx202, vwx212, bhf, bhg)
new_esEs4(Right(vwx200), Right(vwx210), bgb, ty_Int) → new_esEs10(vwx200, vwx210)
new_ltEs13(vwx300, vwx3100) → new_not(new_compare8(vwx300, vwx3100))
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Int) → new_ltEs13(vwx3000, vwx31000)
new_lt6(vwx3001, vwx31001, app(app(ty_@2, hc), hd)) → new_lt19(vwx3001, vwx31001, hc, hd)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Ordering) → new_ltEs14(vwx3000, vwx31000)
new_esEs5(Just(vwx200), Just(vwx210), app(ty_Maybe, cfe)) → new_esEs5(vwx200, vwx210, cfe)
new_esEs15(Integer(vwx200), Integer(vwx210)) → new_primEqInt(vwx200, vwx210)
new_ltEs18(vwx3002, vwx31002, ty_Float) → new_ltEs5(vwx3002, vwx31002)
new_esEs22(vwx200, vwx210, app(ty_Ratio, cbf)) → new_esEs18(vwx200, vwx210, cbf)
new_esEs19(Double(vwx200, vwx201), Double(vwx210, vwx211)) → new_esEs10(new_sr0(vwx200, vwx210), new_sr0(vwx201, vwx211))
new_ltEs6(Just(vwx3000), Just(vwx31000), app(ty_Ratio, bee)) → new_ltEs10(vwx3000, vwx31000, bee)
new_ltEs7(Left(vwx3000), Left(vwx31000), app(app(app(ty_@3, be), bf), bg), bc) → new_ltEs9(vwx3000, vwx31000, be, bf, bg)
new_esEs25(vwx201, vwx211, ty_Float) → new_esEs13(vwx201, vwx211)
new_esEs25(vwx201, vwx211, app(app(ty_@2, chc), chd)) → new_esEs7(vwx201, vwx211, chc, chd)
new_esEs25(vwx201, vwx211, app(app(ty_Either, che), chf)) → new_esEs4(vwx201, vwx211, che, chf)
new_ltEs12(True, False) → False
new_esEs22(vwx200, vwx210, app(app(ty_Either, ccb), ccc)) → new_esEs4(vwx200, vwx210, ccb, ccc)
new_ltEs14(GT, EQ) → False
new_lt5(vwx3000, vwx31000, app(ty_[], fh)) → new_lt16(vwx3000, vwx31000, fh)
new_ltEs6(Just(vwx3000), Just(vwx31000), app(app(app(ty_@3, ea), eb), ec)) → new_ltEs9(vwx3000, vwx31000, ea, eb, ec)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, ty_Bool) → new_ltEs12(vwx3000, vwx31000)
new_compare18(:%(vwx3000, vwx3001), :%(vwx31000, vwx31001), ty_Integer) → new_compare6(new_sr(vwx3000, vwx31001), new_sr(vwx31000, vwx3001))
new_esEs12(vwx20, vwx21, app(ty_[], bfe)) → new_esEs17(vwx20, vwx21, bfe)
new_lt20(vwx3000, vwx31000, app(app(app(ty_@3, bcd), bce), bcf)) → new_lt10(vwx3000, vwx31000, bcd, bce, bcf)
new_compare7(Float(vwx3000, vwx3001), Float(vwx31000, vwx31001)) → new_compare8(new_sr0(vwx3000, vwx31000), new_sr0(vwx3001, vwx31001))
new_esEs7(@2(vwx200, vwx201), @2(vwx210, vwx211), bfh, bga) → new_asAs(new_esEs26(vwx200, vwx210, bfh), new_esEs25(vwx201, vwx211, bga))
new_lt5(vwx3000, vwx31000, app(app(app(ty_@3, fd), ff), fg)) → new_lt10(vwx3000, vwx31000, fd, ff, fg)
new_esEs27(vwx200, vwx210, ty_Ordering) → new_esEs16(vwx200, vwx210)
new_esEs27(vwx200, vwx210, app(ty_[], dbe)) → new_esEs17(vwx200, vwx210, dbe)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, ty_Char) → new_ltEs16(vwx3000, vwx31000)
new_esEs5(Just(vwx200), Just(vwx210), ty_Integer) → new_esEs15(vwx200, vwx210)
new_lt11(vwx3000, vwx31000, bef) → new_esEs9(new_compare18(vwx3000, vwx31000, bef))
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, ty_Int) → new_ltEs13(vwx3000, vwx31000)
new_esEs4(Right(vwx200), Right(vwx210), bgb, ty_Integer) → new_esEs15(vwx200, vwx210)
new_compare9(vwx3000, vwx31000) → new_compare26(vwx3000, vwx31000, new_esEs16(vwx3000, vwx31000))
new_lt5(vwx3000, vwx31000, ty_Int) → new_lt15(vwx3000, vwx31000)
new_esEs21(vwx201, vwx211, ty_@0) → new_esEs8(vwx201, vwx211)
new_lt6(vwx3001, vwx31001, ty_@0) → new_lt9(vwx3001, vwx31001)
new_ltEs18(vwx3002, vwx31002, ty_Int) → new_ltEs13(vwx3002, vwx31002)
new_lt20(vwx3000, vwx31000, app(app(ty_Either, bbh), bca)) → new_lt7(vwx3000, vwx31000, bbh, bca)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, ty_Float) → new_ltEs5(vwx3000, vwx31000)
new_primCmpNat0(Zero, Succ(vwx310000)) → LT
new_esEs4(Right(vwx200), Right(vwx210), bgb, app(app(ty_@2, ced), cee)) → new_esEs7(vwx200, vwx210, ced, cee)
new_esEs21(vwx201, vwx211, ty_Double) → new_esEs19(vwx201, vwx211)
new_esEs26(vwx200, vwx210, ty_Bool) → new_esEs11(vwx200, vwx210)
new_ltEs6(Just(vwx3000), Just(vwx31000), app(app(ty_@2, ee), ef)) → new_ltEs17(vwx3000, vwx31000, ee, ef)
new_lt6(vwx3001, vwx31001, ty_Char) → new_lt18(vwx3001, vwx31001)
new_ltEs6(Just(vwx3000), Just(vwx31000), app(app(ty_Either, df), dg)) → new_ltEs7(vwx3000, vwx31000, df, dg)
new_lt5(vwx3000, vwx31000, ty_Ordering) → new_lt4(vwx3000, vwx31000)
new_esEs25(vwx201, vwx211, ty_Char) → new_esEs14(vwx201, vwx211)
new_esEs20(vwx202, vwx212, ty_Bool) → new_esEs11(vwx202, vwx212)
new_ltEs15(vwx300, vwx3100) → new_not(new_compare16(vwx300, vwx3100))
new_esEs4(Right(vwx200), Right(vwx210), bgb, ty_Char) → new_esEs14(vwx200, vwx210)
new_lt20(vwx3000, vwx31000, app(app(ty_@2, bch), bda)) → new_lt19(vwx3000, vwx31000, bch, bda)
new_esEs20(vwx202, vwx212, app(app(app(ty_@3, bgf), bgg), bgh)) → new_esEs6(vwx202, vwx212, bgf, bgg, bgh)
new_esEs5(Just(vwx200), Just(vwx210), app(ty_[], cfc)) → new_esEs17(vwx200, vwx210, cfc)
new_primEqNat0(Zero, Zero) → True
new_compare14(vwx3000, vwx31000, False, ga, gb) → GT
new_ltEs9(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), gc, fa, fb) → new_pePe(new_lt5(vwx3000, vwx31000, gc), vwx3000, vwx31000, new_pePe(new_lt6(vwx3001, vwx31001, fa), vwx3001, vwx31001, new_ltEs18(vwx3002, vwx31002, fb), fa), gc)
new_ltEs19(vwx3001, vwx31001, ty_Int) → new_ltEs13(vwx3001, vwx31001)
new_compare26(vwx3000, vwx31000, True) → EQ
new_ltEs12(False, False) → True
new_lt20(vwx3000, vwx31000, ty_Int) → new_lt15(vwx3000, vwx31000)
new_esEs16(GT, LT) → False
new_esEs16(LT, GT) → False
new_ltEs19(vwx3001, vwx31001, app(ty_[], bea)) → new_ltEs4(vwx3001, vwx31001, bea)
new_compare27(vwx3000, vwx31000, False) → new_compare11(vwx3000, vwx31000, new_ltEs12(vwx3000, vwx31000))
new_esEs22(vwx200, vwx210, app(app(ty_@2, cbh), cca)) → new_esEs7(vwx200, vwx210, cbh, cca)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_@0) → new_ltEs8(vwx3000, vwx31000)
new_ltEs11(vwx300, vwx3100) → new_not(new_compare6(vwx300, vwx3100))
new_esEs5(Just(vwx200), Just(vwx210), ty_Ordering) → new_esEs16(vwx200, vwx210)
new_ltEs17(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), bdb, bcb) → new_pePe(new_lt20(vwx3000, vwx31000, bdb), vwx3000, vwx31000, new_ltEs19(vwx3001, vwx31001, bcb), bdb)
new_compare32(vwx3000, vwx31000, app(app(ty_@2, bbf), bbg)) → new_compare29(vwx3000, vwx31000, bbf, bbg)
new_esEs12(vwx20, vwx21, app(app(ty_@2, bfh), bga)) → new_esEs7(vwx20, vwx21, bfh, bga)
new_ltEs14(EQ, LT) → False
new_esEs4(Left(vwx200), Left(vwx210), app(ty_[], ccg), bgc) → new_esEs17(vwx200, vwx210, ccg)
new_ltEs18(vwx3002, vwx31002, app(app(app(ty_@3, hh), baa), bab)) → new_ltEs9(vwx3002, vwx31002, hh, baa, bab)
new_compare4([], [], baf) → EQ
new_primPlusNat0(Succ(vwx650), vwx3100100) → Succ(Succ(new_primPlusNat1(vwx650, vwx3100100)))
new_compare29(vwx3000, vwx31000, ga, gb) → new_compare23(vwx3000, vwx31000, new_esEs7(vwx3000, vwx31000, ga, gb), ga, gb)
new_esEs4(Right(vwx200), Right(vwx210), bgb, ty_@0) → new_esEs8(vwx200, vwx210)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Integer) → new_ltEs11(vwx3000, vwx31000)
new_lt20(vwx3000, vwx31000, ty_Double) → new_lt17(vwx3000, vwx31000)
new_esEs26(vwx200, vwx210, app(app(app(ty_@3, chg), chh), daa)) → new_esEs6(vwx200, vwx210, chg, chh, daa)
new_ltEs19(vwx3001, vwx31001, ty_Bool) → new_ltEs12(vwx3001, vwx31001)
new_lt12(vwx3000, vwx31000) → new_esEs9(new_compare6(vwx3000, vwx31000))
new_esEs4(Right(vwx200), Right(vwx210), bgb, app(app(ty_Either, cef), ceg)) → new_esEs4(vwx200, vwx210, cef, ceg)
new_esEs22(vwx200, vwx210, ty_Char) → new_esEs14(vwx200, vwx210)
new_compare24(vwx3000, vwx31000, True, fd, ff, fg) → EQ
new_primEqInt(Neg(Succ(vwx2000)), Neg(Succ(vwx2100))) → new_primEqNat0(vwx2000, vwx2100)
new_ltEs19(vwx3001, vwx31001, app(app(ty_@2, beb), bec)) → new_ltEs17(vwx3001, vwx31001, beb, bec)
new_lt20(vwx3000, vwx31000, app(ty_Ratio, bgd)) → new_lt11(vwx3000, vwx31000, bgd)
new_ltEs18(vwx3002, vwx31002, app(ty_Ratio, beh)) → new_ltEs10(vwx3002, vwx31002, beh)
new_esEs25(vwx201, vwx211, ty_Bool) → new_esEs11(vwx201, vwx211)
new_esEs4(Right(vwx200), Right(vwx210), bgb, app(ty_[], cea)) → new_esEs17(vwx200, vwx210, cea)
new_esEs9(GT) → False
new_esEs22(vwx200, vwx210, app(app(app(ty_@3, cbb), cbc), cbd)) → new_esEs6(vwx200, vwx210, cbb, cbc, cbd)
new_lt16(vwx3000, vwx31000, fh) → new_esEs9(new_compare4(vwx3000, vwx31000, fh))
new_ltEs18(vwx3002, vwx31002, app(app(ty_Either, he), hf)) → new_ltEs7(vwx3002, vwx31002, he, hf)
new_esEs4(Left(vwx200), Left(vwx210), app(app(ty_Either, cdd), cde), bgc) → new_esEs4(vwx200, vwx210, cdd, cde)
new_ltEs19(vwx3001, vwx31001, app(app(app(ty_@3, bdf), bdg), bdh)) → new_ltEs9(vwx3001, vwx31001, bdf, bdg, bdh)
new_primPlusNat1(Zero, Succ(vwx31001000)) → Succ(vwx31001000)
new_primPlusNat1(Succ(vwx6500), Zero) → Succ(vwx6500)
new_esEs6(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), bfb, bfc, bfd) → new_asAs(new_esEs22(vwx200, vwx210, bfb), new_asAs(new_esEs21(vwx201, vwx211, bfc), new_esEs20(vwx202, vwx212, bfd)))
new_lt5(vwx3000, vwx31000, ty_Integer) → new_lt12(vwx3000, vwx31000)
new_esEs9(EQ) → False
new_esEs4(Left(vwx200), Left(vwx210), ty_Int, bgc) → new_esEs10(vwx200, vwx210)
new_lt6(vwx3001, vwx31001, ty_Bool) → new_lt13(vwx3001, vwx31001)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_ltEs7(Right(vwx3000), Left(vwx31000), cc, bc) → False
new_esEs5(Just(vwx200), Just(vwx210), ty_Int) → new_esEs10(vwx200, vwx210)
new_lt6(vwx3001, vwx31001, ty_Ordering) → new_lt4(vwx3001, vwx31001)
new_ltEs5(vwx300, vwx3100) → new_not(new_compare7(vwx300, vwx3100))
new_lt6(vwx3001, vwx31001, app(ty_Ratio, beg)) → new_lt11(vwx3001, vwx31001, beg)
new_esEs21(vwx201, vwx211, app(app(ty_@2, caf), cag)) → new_esEs7(vwx201, vwx211, caf, cag)
new_esEs20(vwx202, vwx212, ty_Float) → new_esEs13(vwx202, vwx212)
new_compare8(vwx300, vwx3100) → new_primCmpInt(vwx300, vwx3100)
new_primEqInt(Neg(Zero), Neg(Succ(vwx2100))) → False
new_primEqInt(Neg(Succ(vwx2000)), Neg(Zero)) → False
new_lt18(vwx3000, vwx31000) → new_esEs9(new_compare19(vwx3000, vwx31000))
new_lt5(vwx3000, vwx31000, ty_@0) → new_lt9(vwx3000, vwx31000)
new_lt6(vwx3001, vwx31001, app(ty_Maybe, gf)) → new_lt8(vwx3001, vwx31001, gf)
new_esEs22(vwx200, vwx210, ty_Float) → new_esEs13(vwx200, vwx210)
new_esEs21(vwx201, vwx211, app(app(ty_Either, cah), cba)) → new_esEs4(vwx201, vwx211, cah, cba)
new_esEs21(vwx201, vwx211, ty_Ordering) → new_esEs16(vwx201, vwx211)
new_compare32(vwx3000, vwx31000, ty_Double) → new_compare16(vwx3000, vwx31000)
new_primCmpInt(Neg(Zero), Pos(Zero)) → EQ
new_primCmpInt(Pos(Zero), Neg(Zero)) → EQ
new_compare210(vwx3000, vwx31000, False, fc) → new_compare110(vwx3000, vwx31000, new_ltEs6(vwx3000, vwx31000, fc), fc)
new_ltEs18(vwx3002, vwx31002, ty_@0) → new_ltEs8(vwx3002, vwx31002)
new_primCmpNat0(Succ(vwx30000), Succ(vwx310000)) → new_primCmpNat0(vwx30000, vwx310000)
new_esEs11(False, False) → True
new_primEqInt(Pos(Succ(vwx2000)), Pos(Succ(vwx2100))) → new_primEqNat0(vwx2000, vwx2100)
new_esEs25(vwx201, vwx211, app(ty_Maybe, chb)) → new_esEs5(vwx201, vwx211, chb)
new_esEs20(vwx202, vwx212, ty_Int) → new_esEs10(vwx202, vwx212)
new_esEs26(vwx200, vwx210, ty_Integer) → new_esEs15(vwx200, vwx210)
new_esEs22(vwx200, vwx210, ty_Double) → new_esEs19(vwx200, vwx210)
new_esEs5(Just(vwx200), Just(vwx210), ty_Bool) → new_esEs11(vwx200, vwx210)
new_ltEs19(vwx3001, vwx31001, app(ty_Ratio, bge)) → new_ltEs10(vwx3001, vwx31001, bge)
new_primEqNat0(Succ(vwx2000), Succ(vwx2100)) → new_primEqNat0(vwx2000, vwx2100)
new_esEs4(Left(vwx200), Left(vwx210), ty_Ordering, bgc) → new_esEs16(vwx200, vwx210)
new_esEs12(vwx20, vwx21, ty_Float) → new_esEs13(vwx20, vwx21)
new_compare32(vwx3000, vwx31000, app(app(app(ty_@3, bbb), bbc), bbd)) → new_compare30(vwx3000, vwx31000, bbb, bbc, bbd)
new_primCompAux00(vwx51, LT) → LT
new_esEs26(vwx200, vwx210, ty_@0) → new_esEs8(vwx200, vwx210)
new_primCmpInt(Neg(Succ(vwx30000)), Neg(vwx31000)) → new_primCmpNat0(vwx31000, Succ(vwx30000))
new_ltEs19(vwx3001, vwx31001, app(app(ty_Either, bdc), bdd)) → new_ltEs7(vwx3001, vwx31001, bdc, bdd)
new_lt19(vwx3000, vwx31000, ga, gb) → new_esEs9(new_compare29(vwx3000, vwx31000, ga, gb))
new_esEs12(vwx20, vwx21, app(app(ty_Either, bgb), bgc)) → new_esEs4(vwx20, vwx21, bgb, bgc)
new_esEs12(vwx20, vwx21, app(ty_Ratio, bff)) → new_esEs18(vwx20, vwx21, bff)
new_compare19(Char(vwx3000), Char(vwx31000)) → new_primCmpNat0(vwx3000, vwx31000)
new_primEqInt(Pos(Zero), Pos(Succ(vwx2100))) → False
new_primEqInt(Pos(Succ(vwx2000)), Pos(Zero)) → False
new_ltEs18(vwx3002, vwx31002, ty_Integer) → new_ltEs11(vwx3002, vwx31002)
new_ltEs19(vwx3001, vwx31001, app(ty_Maybe, bde)) → new_ltEs6(vwx3001, vwx31001, bde)
new_lt20(vwx3000, vwx31000, ty_Char) → new_lt18(vwx3000, vwx31000)
new_ltEs6(Just(vwx3000), Nothing, bed) → False
new_primCmpNat0(Zero, Zero) → EQ
new_primCmpNat0(Succ(vwx30000), Zero) → GT
new_compare31(vwx3000, vwx31000, eg, eh) → new_compare25(vwx3000, vwx31000, new_esEs4(vwx3000, vwx31000, eg, eh), eg, eh)
new_primCmpInt(Neg(Zero), Pos(Succ(vwx310000))) → LT
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, ty_Double) → new_ltEs15(vwx3000, vwx31000)
new_ltEs6(Just(vwx3000), Just(vwx31000), app(ty_[], ed)) → new_ltEs4(vwx3000, vwx31000, ed)
new_primPlusNat1(Succ(vwx6500), Succ(vwx31001000)) → Succ(Succ(new_primPlusNat1(vwx6500, vwx31001000)))
new_compare6(Integer(vwx3000), Integer(vwx31000)) → new_primCmpInt(vwx3000, vwx31000)
new_primEqInt(Neg(Succ(vwx2000)), Pos(vwx210)) → False
new_primEqInt(Pos(Succ(vwx2000)), Neg(vwx210)) → False
new_esEs25(vwx201, vwx211, ty_Int) → new_esEs10(vwx201, vwx211)
new_compare210(vwx3000, vwx31000, True, fc) → EQ
new_esEs27(vwx200, vwx210, app(ty_Maybe, dbg)) → new_esEs5(vwx200, vwx210, dbg)
new_esEs25(vwx201, vwx211, ty_@0) → new_esEs8(vwx201, vwx211)
new_ltEs6(Just(vwx3000), Just(vwx31000), app(ty_Maybe, dh)) → new_ltEs6(vwx3000, vwx31000, dh)
new_primEqInt(Neg(Zero), Pos(Succ(vwx2100))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vwx2100))) → False
new_esEs26(vwx200, vwx210, ty_Int) → new_esEs10(vwx200, vwx210)
new_esEs26(vwx200, vwx210, app(ty_[], dab)) → new_esEs17(vwx200, vwx210, dab)
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Char, bc) → new_ltEs16(vwx3000, vwx31000)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, app(ty_[], dc)) → new_ltEs4(vwx3000, vwx31000, dc)
new_esEs21(vwx201, vwx211, ty_Integer) → new_esEs15(vwx201, vwx211)
new_primCmpInt(Pos(Zero), Pos(Succ(vwx310000))) → new_primCmpNat0(Zero, Succ(vwx310000))
new_primCompAux00(vwx51, EQ) → vwx51
new_esEs27(vwx200, vwx210, app(app(ty_@2, dbh), dca)) → new_esEs7(vwx200, vwx210, dbh, dca)
new_lt6(vwx3001, vwx31001, app(ty_[], hb)) → new_lt16(vwx3001, vwx31001, hb)
new_lt20(vwx3000, vwx31000, ty_Bool) → new_lt13(vwx3000, vwx31000)
new_lt20(vwx3000, vwx31000, ty_Ordering) → new_lt4(vwx3000, vwx31000)
new_esEs4(Right(vwx200), Right(vwx210), bgb, ty_Ordering) → new_esEs16(vwx200, vwx210)
new_esEs22(vwx200, vwx210, ty_@0) → new_esEs8(vwx200, vwx210)
new_esEs4(Left(vwx200), Left(vwx210), ty_Integer, bgc) → new_esEs15(vwx200, vwx210)
new_lt7(vwx3000, vwx31000, eg, eh) → new_esEs9(new_compare31(vwx3000, vwx31000, eg, eh))
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Int, bc) → new_ltEs13(vwx3000, vwx31000)
new_compare32(vwx3000, vwx31000, app(ty_Maybe, bba)) → new_compare28(vwx3000, vwx31000, bba)
new_pePe(False, vwx20, vwx21, vwx37, bfa) → new_asAs(new_esEs12(vwx20, vwx21, bfa), vwx37)
new_esEs21(vwx201, vwx211, app(ty_[], cac)) → new_esEs17(vwx201, vwx211, cac)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, app(ty_Ratio, cgd)) → new_ltEs10(vwx3000, vwx31000, cgd)
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Double, bc) → new_ltEs15(vwx3000, vwx31000)
new_compare12(@0, @0) → EQ
new_compare32(vwx3000, vwx31000, app(ty_[], bbe)) → new_compare4(vwx3000, vwx31000, bbe)
new_primCmpInt(Pos(Succ(vwx30000)), Pos(vwx31000)) → new_primCmpNat0(Succ(vwx30000), vwx31000)
new_primPlusNat0(Zero, vwx3100100) → Succ(vwx3100100)
new_compare110(vwx3000, vwx31000, True, fc) → LT
new_esEs5(Just(vwx200), Just(vwx210), ty_Char) → new_esEs14(vwx200, vwx210)
new_compare32(vwx3000, vwx31000, ty_Char) → new_compare19(vwx3000, vwx31000)
new_ltEs7(Left(vwx3000), Left(vwx31000), app(ty_Ratio, cgc), bc) → new_ltEs10(vwx3000, vwx31000, cgc)
new_ltEs19(vwx3001, vwx31001, ty_Float) → new_ltEs5(vwx3001, vwx31001)
new_ltEs7(Left(vwx3000), Left(vwx31000), app(ty_Maybe, bd), bc) → new_ltEs6(vwx3000, vwx31000, bd)
new_esEs20(vwx202, vwx212, ty_Char) → new_esEs14(vwx202, vwx212)
new_esEs26(vwx200, vwx210, app(ty_Ratio, dac)) → new_esEs18(vwx200, vwx210, dac)
new_esEs25(vwx201, vwx211, ty_Integer) → new_esEs15(vwx201, vwx211)
new_esEs16(EQ, LT) → False
new_esEs16(LT, EQ) → False
new_ltEs18(vwx3002, vwx31002, ty_Ordering) → new_ltEs14(vwx3002, vwx31002)
new_ltEs14(LT, LT) → True
new_lt5(vwx3000, vwx31000, ty_Bool) → new_lt13(vwx3000, vwx31000)
new_not0True
new_compare32(vwx3000, vwx31000, ty_@0) → new_compare12(vwx3000, vwx31000)
new_esEs8(@0, @0) → True
new_lt6(vwx3001, vwx31001, ty_Int) → new_lt15(vwx3001, vwx31001)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, ty_@0) → new_ltEs8(vwx3000, vwx31000)
new_ltEs18(vwx3002, vwx31002, ty_Bool) → new_ltEs12(vwx3002, vwx31002)
new_ltEs10(vwx300, vwx3100, cgb) → new_not(new_compare18(vwx300, vwx3100, cgb))
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Bool) → new_ltEs12(vwx3000, vwx31000)
new_esEs22(vwx200, vwx210, ty_Bool) → new_esEs11(vwx200, vwx210)
new_primCmpInt(Pos(Succ(vwx30000)), Neg(vwx31000)) → GT
new_esEs12(vwx20, vwx21, ty_@0) → new_esEs8(vwx20, vwx21)
new_lt5(vwx3000, vwx31000, app(ty_Ratio, bef)) → new_lt11(vwx3000, vwx31000, bef)
new_primMulInt(Pos(vwx30000), Pos(vwx310010)) → Pos(new_primMulNat0(vwx30000, vwx310010))
new_lt9(vwx3000, vwx31000) → new_esEs9(new_compare12(vwx3000, vwx31000))
new_esEs27(vwx200, vwx210, ty_Bool) → new_esEs11(vwx200, vwx210)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, ty_Ordering) → new_ltEs14(vwx3000, vwx31000)
new_esEs12(vwx20, vwx21, ty_Bool) → new_esEs11(vwx20, vwx21)
new_esEs22(vwx200, vwx210, ty_Int) → new_esEs10(vwx200, vwx210)
new_primMulInt(Neg(vwx30000), Neg(vwx310010)) → Pos(new_primMulNat0(vwx30000, vwx310010))
new_lt14(vwx3000, vwx31000) → new_esEs9(new_compare7(vwx3000, vwx31000))
new_esEs16(EQ, EQ) → True
new_esEs20(vwx202, vwx212, ty_Integer) → new_esEs15(vwx202, vwx212)
new_esEs26(vwx200, vwx210, ty_Ordering) → new_esEs16(vwx200, vwx210)
new_primEqNat0(Zero, Succ(vwx2100)) → False
new_primEqNat0(Succ(vwx2000), Zero) → False
new_esEs5(Just(vwx200), Just(vwx210), app(ty_Ratio, cfd)) → new_esEs18(vwx200, vwx210, cfd)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, ty_Integer) → new_ltEs11(vwx3000, vwx31000)
new_esEs27(vwx200, vwx210, ty_Char) → new_esEs14(vwx200, vwx210)
new_esEs26(vwx200, vwx210, app(app(ty_@2, dae), daf)) → new_esEs7(vwx200, vwx210, dae, daf)
new_ltEs7(Left(vwx3000), Left(vwx31000), app(app(ty_Either, ba), bb), bc) → new_ltEs7(vwx3000, vwx31000, ba, bb)
new_compare25(vwx3000, vwx31000, True, eg, eh) → EQ
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs12(vwx20, vwx21, ty_Double) → new_esEs19(vwx20, vwx21)
new_esEs27(vwx200, vwx210, app(app(ty_Either, dcb), dcc)) → new_esEs4(vwx200, vwx210, dcb, dcc)
new_esEs27(vwx200, vwx210, app(app(app(ty_@3, dbb), dbc), dbd)) → new_esEs6(vwx200, vwx210, dbb, dbc, dbd)
new_compare4(:(vwx3000, vwx3001), [], baf) → GT
new_esEs20(vwx202, vwx212, app(ty_[], bha)) → new_esEs17(vwx202, vwx212, bha)
new_compare28(vwx3000, vwx31000, fc) → new_compare210(vwx3000, vwx31000, new_esEs5(vwx3000, vwx31000, fc), fc)
new_esEs22(vwx200, vwx210, app(ty_[], cbe)) → new_esEs17(vwx200, vwx210, cbe)
new_ltEs18(vwx3002, vwx31002, app(app(ty_@2, bad), bae)) → new_ltEs17(vwx3002, vwx31002, bad, bae)
new_esEs26(vwx200, vwx210, app(ty_Maybe, dad)) → new_esEs5(vwx200, vwx210, dad)
new_pePe(True, vwx20, vwx21, vwx37, bfa) → True
new_esEs5(Just(vwx200), Just(vwx210), ty_Double) → new_esEs19(vwx200, vwx210)
new_compare25(vwx3000, vwx31000, False, eg, eh) → new_compare15(vwx3000, vwx31000, new_ltEs7(vwx3000, vwx31000, eg, eh), eg, eh)
new_lt20(vwx3000, vwx31000, ty_@0) → new_lt9(vwx3000, vwx31000)
new_primCmpInt(Neg(Zero), Neg(Succ(vwx310000))) → new_primCmpNat0(Succ(vwx310000), Zero)
new_compare23(vwx3000, vwx31000, True, ga, gb) → EQ
new_primCmpInt(Pos(Zero), Neg(Succ(vwx310000))) → GT
new_esEs11(True, False) → False
new_esEs11(False, True) → False
new_compare110(vwx3000, vwx31000, False, fc) → GT
new_esEs5(Just(vwx200), Just(vwx210), app(app(app(ty_@3, ceh), cfa), cfb)) → new_esEs6(vwx200, vwx210, ceh, cfa, cfb)
new_lt6(vwx3001, vwx31001, ty_Double) → new_lt17(vwx3001, vwx31001)
new_compare4([], :(vwx31000, vwx31001), baf) → LT
new_lt5(vwx3000, vwx31000, ty_Float) → new_lt14(vwx3000, vwx31000)
new_sr0(vwx3000, vwx31001) → new_primMulInt(vwx3000, vwx31001)
new_compare15(vwx3000, vwx31000, False, eg, eh) → GT
new_compare32(vwx3000, vwx31000, ty_Int) → new_compare8(vwx3000, vwx31000)
new_compare17(vwx3000, vwx31000) → new_compare27(vwx3000, vwx31000, new_esEs11(vwx3000, vwx31000))
new_esEs20(vwx202, vwx212, app(ty_Ratio, bhb)) → new_esEs18(vwx202, vwx212, bhb)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Double) → new_ltEs15(vwx3000, vwx31000)
new_ltEs19(vwx3001, vwx31001, ty_Ordering) → new_ltEs14(vwx3001, vwx31001)
new_ltEs7(Left(vwx3000), Left(vwx31000), app(ty_[], bh), bc) → new_ltEs4(vwx3000, vwx31000, bh)
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Integer, bc) → new_ltEs11(vwx3000, vwx31000)
new_lt6(vwx3001, vwx31001, ty_Float) → new_lt14(vwx3001, vwx31001)
new_ltEs19(vwx3001, vwx31001, ty_Integer) → new_ltEs11(vwx3001, vwx31001)
new_esEs25(vwx201, vwx211, ty_Ordering) → new_esEs16(vwx201, vwx211)
new_lt20(vwx3000, vwx31000, app(ty_[], bcg)) → new_lt16(vwx3000, vwx31000, bcg)
new_esEs21(vwx201, vwx211, ty_Bool) → new_esEs11(vwx201, vwx211)
new_compare32(vwx3000, vwx31000, ty_Bool) → new_compare17(vwx3000, vwx31000)
new_esEs21(vwx201, vwx211, ty_Float) → new_esEs13(vwx201, vwx211)
new_primCmpInt(Neg(Zero), Neg(Zero)) → EQ
new_esEs27(vwx200, vwx210, ty_Float) → new_esEs13(vwx200, vwx210)
new_esEs24(vwx200, vwx210, ty_Int) → new_esEs10(vwx200, vwx210)
new_esEs20(vwx202, vwx212, app(ty_Maybe, bhc)) → new_esEs5(vwx202, vwx212, bhc)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, app(app(ty_Either, cd), ce)) → new_ltEs7(vwx3000, vwx31000, cd, ce)
new_esEs16(LT, LT) → True
new_asAs(False, vwx46) → False
new_esEs18(:%(vwx200, vwx201), :%(vwx210, vwx211), bff) → new_asAs(new_esEs24(vwx200, vwx210, bff), new_esEs23(vwx201, vwx211, bff))
new_lt6(vwx3001, vwx31001, ty_Integer) → new_lt12(vwx3001, vwx31001)
new_ltEs18(vwx3002, vwx31002, ty_Double) → new_ltEs15(vwx3002, vwx31002)
new_primMulInt(Neg(vwx30000), Pos(vwx310010)) → Neg(new_primMulNat0(vwx30000, vwx310010))
new_primMulInt(Pos(vwx30000), Neg(vwx310010)) → Neg(new_primMulNat0(vwx30000, vwx310010))
new_primMulNat0(Succ(vwx300000), Zero) → Zero
new_primMulNat0(Zero, Succ(vwx3100100)) → Zero
new_lt5(vwx3000, vwx31000, app(app(ty_@2, ga), gb)) → new_lt19(vwx3000, vwx31000, ga, gb)
new_compare23(vwx3000, vwx31000, False, ga, gb) → new_compare14(vwx3000, vwx31000, new_ltEs17(vwx3000, vwx31000, ga, gb), ga, gb)
new_esEs22(vwx200, vwx210, ty_Ordering) → new_esEs16(vwx200, vwx210)
new_compare4(:(vwx3000, vwx3001), :(vwx31000, vwx31001), baf) → new_primCompAux0(vwx3000, vwx31000, new_compare4(vwx3001, vwx31001, baf), baf)
new_esEs16(GT, GT) → True
new_ltEs18(vwx3002, vwx31002, app(ty_[], bac)) → new_ltEs4(vwx3002, vwx31002, bac)
new_ltEs19(vwx3001, vwx31001, ty_Char) → new_ltEs16(vwx3001, vwx31001)
new_esEs12(vwx20, vwx21, ty_Char) → new_esEs14(vwx20, vwx21)
new_ltEs14(GT, LT) → False
new_esEs17(:(vwx200, vwx201), :(vwx210, vwx211), bfe) → new_asAs(new_esEs27(vwx200, vwx210, bfe), new_esEs17(vwx201, vwx211, bfe))
new_not(EQ) → new_not0
new_ltEs12(True, True) → True
new_esEs4(Left(vwx200), Left(vwx210), app(ty_Maybe, cda), bgc) → new_esEs5(vwx200, vwx210, cda)
new_esEs25(vwx201, vwx211, app(ty_[], cgh)) → new_esEs17(vwx201, vwx211, cgh)
new_esEs11(True, True) → True
new_lt5(vwx3000, vwx31000, ty_Double) → new_lt17(vwx3000, vwx31000)
new_esEs25(vwx201, vwx211, app(app(app(ty_@3, cge), cgf), cgg)) → new_esEs6(vwx201, vwx211, cge, cgf, cgg)
new_ltEs12(False, True) → True
new_compare24(vwx3000, vwx31000, False, fd, ff, fg) → new_compare13(vwx3000, vwx31000, new_ltEs9(vwx3000, vwx31000, fd, ff, fg), fd, ff, fg)
new_esEs5(Just(vwx200), Just(vwx210), ty_@0) → new_esEs8(vwx200, vwx210)
new_esEs23(vwx201, vwx211, ty_Integer) → new_esEs15(vwx201, vwx211)
new_compare27(vwx3000, vwx31000, True) → EQ
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, app(app(ty_@2, dd), de)) → new_ltEs17(vwx3000, vwx31000, dd, de)
new_esEs26(vwx200, vwx210, ty_Double) → new_esEs19(vwx200, vwx210)
new_ltEs19(vwx3001, vwx31001, ty_@0) → new_ltEs8(vwx3001, vwx31001)
new_esEs5(Just(vwx200), Nothing, bfg) → False
new_esEs5(Nothing, Just(vwx210), bfg) → False
new_esEs14(Char(vwx200), Char(vwx210)) → new_primEqNat0(vwx200, vwx210)
new_ltEs6(Nothing, Nothing, bed) → True
new_esEs4(Left(vwx200), Left(vwx210), ty_Float, bgc) → new_esEs13(vwx200, vwx210)
new_esEs12(vwx20, vwx21, app(app(app(ty_@3, bfb), bfc), bfd)) → new_esEs6(vwx20, vwx21, bfb, bfc, bfd)
new_ltEs16(vwx300, vwx3100) → new_not(new_compare19(vwx300, vwx3100))
new_esEs5(Just(vwx200), Just(vwx210), ty_Float) → new_esEs13(vwx200, vwx210)
new_esEs4(Left(vwx200), Left(vwx210), app(app(ty_@2, cdb), cdc), bgc) → new_esEs7(vwx200, vwx210, cdb, cdc)
new_esEs12(vwx20, vwx21, ty_Int) → new_esEs10(vwx20, vwx21)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, app(app(app(ty_@3, cg), da), db)) → new_ltEs9(vwx3000, vwx31000, cg, da, db)
new_compare26(vwx3000, vwx31000, False) → new_compare10(vwx3000, vwx31000, new_ltEs14(vwx3000, vwx31000))
new_compare11(vwx3000, vwx31000, False) → GT
new_compare30(vwx3000, vwx31000, fd, ff, fg) → new_compare24(vwx3000, vwx31000, new_esEs6(vwx3000, vwx31000, fd, ff, fg), fd, ff, fg)
new_ltEs14(LT, GT) → True
new_ltEs8(vwx300, vwx3100) → new_not(new_compare12(vwx300, vwx3100))
new_lt20(vwx3000, vwx31000, ty_Integer) → new_lt12(vwx3000, vwx31000)
new_not(LT) → new_not0
new_ltEs14(LT, EQ) → True
new_compare11(vwx3000, vwx31000, True) → LT
new_esEs5(Nothing, Nothing, bfg) → True
new_ltEs18(vwx3002, vwx31002, app(ty_Maybe, hg)) → new_ltEs6(vwx3002, vwx31002, hg)
new_compare14(vwx3000, vwx31000, True, ga, gb) → LT
new_esEs4(Left(vwx200), Left(vwx210), ty_Char, bgc) → new_esEs14(vwx200, vwx210)
new_compare32(vwx3000, vwx31000, ty_Ordering) → new_compare9(vwx3000, vwx31000)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Float) → new_ltEs5(vwx3000, vwx31000)
new_lt6(vwx3001, vwx31001, app(app(ty_Either, gd), ge)) → new_lt7(vwx3001, vwx31001, gd, ge)
new_ltEs19(vwx3001, vwx31001, ty_Double) → new_ltEs15(vwx3001, vwx31001)
new_esEs4(Right(vwx200), Right(vwx210), bgb, ty_Double) → new_esEs19(vwx200, vwx210)
new_compare32(vwx3000, vwx31000, ty_Float) → new_compare7(vwx3000, vwx31000)
new_esEs20(vwx202, vwx212, app(app(ty_@2, bhd), bhe)) → new_esEs7(vwx202, vwx212, bhd, bhe)
new_esEs25(vwx201, vwx211, ty_Double) → new_esEs19(vwx201, vwx211)
new_esEs22(vwx200, vwx210, app(ty_Maybe, cbg)) → new_esEs5(vwx200, vwx210, cbg)
new_lt20(vwx3000, vwx31000, app(ty_Maybe, bcc)) → new_lt8(vwx3000, vwx31000, bcc)
new_esEs21(vwx201, vwx211, app(ty_Maybe, cae)) → new_esEs5(vwx201, vwx211, cae)
new_esEs22(vwx200, vwx210, ty_Integer) → new_esEs15(vwx200, vwx210)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs21(vwx201, vwx211, app(app(app(ty_@3, bhh), caa), cab)) → new_esEs6(vwx201, vwx211, bhh, caa, cab)
new_compare32(vwx3000, vwx31000, app(app(ty_Either, bag), bah)) → new_compare31(vwx3000, vwx31000, bag, bah)
new_esEs4(Left(vwx200), Left(vwx210), ty_Bool, bgc) → new_esEs11(vwx200, vwx210)
new_compare16(Double(vwx3000, vwx3001), Double(vwx31000, vwx31001)) → new_compare8(new_sr0(vwx3000, vwx31000), new_sr0(vwx3001, vwx31001))
new_esEs26(vwx200, vwx210, app(app(ty_Either, dag), dah)) → new_esEs4(vwx200, vwx210, dag, dah)
new_esEs12(vwx20, vwx21, ty_Ordering) → new_esEs16(vwx20, vwx21)
new_asAs(True, vwx46) → vwx46
new_ltEs14(EQ, EQ) → True
new_esEs12(vwx20, vwx21, ty_Integer) → new_esEs15(vwx20, vwx21)
new_lt15(vwx3000, vwx31000) → new_esEs9(new_compare8(vwx3000, vwx31000))
new_primMulNat0(Succ(vwx300000), Succ(vwx3100100)) → new_primPlusNat0(new_primMulNat0(vwx300000, Succ(vwx3100100)), vwx3100100)
new_lt13(vwx3000, vwx31000) → new_esEs9(new_compare17(vwx3000, vwx31000))
new_esEs4(Left(vwx200), Right(vwx210), bgb, bgc) → False
new_esEs4(Right(vwx200), Left(vwx210), bgb, bgc) → False
new_esEs5(Just(vwx200), Just(vwx210), app(app(ty_@2, cff), cfg)) → new_esEs7(vwx200, vwx210, cff, cfg)
new_esEs27(vwx200, vwx210, ty_Int) → new_esEs10(vwx200, vwx210)
new_esEs21(vwx201, vwx211, ty_Char) → new_esEs14(vwx201, vwx211)
new_esEs23(vwx201, vwx211, ty_Int) → new_esEs10(vwx201, vwx211)
new_esEs21(vwx201, vwx211, ty_Int) → new_esEs10(vwx201, vwx211)
new_esEs4(Left(vwx200), Left(vwx210), app(app(app(ty_@3, ccd), cce), ccf), bgc) → new_esEs6(vwx200, vwx210, ccd, cce, ccf)
new_esEs17([], [], bfe) → True
new_compare32(vwx3000, vwx31000, ty_Integer) → new_compare6(vwx3000, vwx31000)
new_esEs17(:(vwx200, vwx201), [], bfe) → False
new_esEs17([], :(vwx210, vwx211), bfe) → False
new_esEs27(vwx200, vwx210, ty_@0) → new_esEs8(vwx200, vwx210)
new_esEs4(Right(vwx200), Right(vwx210), bgb, ty_Float) → new_esEs13(vwx200, vwx210)
new_esEs13(Float(vwx200, vwx201), Float(vwx210, vwx211)) → new_esEs10(new_sr0(vwx200, vwx210), new_sr0(vwx201, vwx211))
new_lt10(vwx3000, vwx31000, fd, ff, fg) → new_esEs9(new_compare30(vwx3000, vwx31000, fd, ff, fg))
new_esEs4(Left(vwx200), Left(vwx210), ty_@0, bgc) → new_esEs8(vwx200, vwx210)
new_compare10(vwx3000, vwx31000, True) → LT
new_lt5(vwx3000, vwx31000, ty_Char) → new_lt18(vwx3000, vwx31000)
new_ltEs7(Right(vwx3000), Right(vwx31000), cc, app(ty_Maybe, cf)) → new_ltEs6(vwx3000, vwx31000, cf)
new_compare32(vwx3000, vwx31000, app(ty_Ratio, dba)) → new_compare18(vwx3000, vwx31000, dba)
new_ltEs4(vwx300, vwx3100, baf) → new_not(new_compare4(vwx300, vwx3100, baf))
new_compare13(vwx3000, vwx31000, True, fd, ff, fg) → LT
new_compare10(vwx3000, vwx31000, False) → GT
new_esEs10(vwx20, vwx21) → new_primEqInt(vwx20, vwx21)
new_lt5(vwx3000, vwx31000, app(ty_Maybe, fc)) → new_lt8(vwx3000, vwx31000, fc)
new_primCompAux00(vwx51, GT) → GT
new_esEs5(Just(vwx200), Just(vwx210), app(app(ty_Either, cfh), cga)) → new_esEs4(vwx200, vwx210, cfh, cga)
new_primCmpInt(Pos(Zero), Pos(Zero)) → EQ
new_compare18(:%(vwx3000, vwx3001), :%(vwx31000, vwx31001), ty_Int) → new_compare8(new_sr0(vwx3000, vwx31001), new_sr0(vwx31000, vwx3001))
new_ltEs14(EQ, GT) → True
new_esEs12(vwx20, vwx21, app(ty_Maybe, bfg)) → new_esEs5(vwx20, vwx21, bfg)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs27(vwx200, vwx210, ty_Integer) → new_esEs15(vwx200, vwx210)
new_esEs21(vwx201, vwx211, app(ty_Ratio, cad)) → new_esEs18(vwx201, vwx211, cad)
new_esEs4(Left(vwx200), Left(vwx210), app(ty_Ratio, cch), bgc) → new_esEs18(vwx200, vwx210, cch)
new_primCmpInt(Neg(Succ(vwx30000)), Pos(vwx31000)) → LT
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Bool, bc) → new_ltEs12(vwx3000, vwx31000)
new_esEs27(vwx200, vwx210, ty_Double) → new_esEs19(vwx200, vwx210)

The set Q consists of the following terms:

new_lt20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primCmpInt(Neg(Zero), Pos(Succ(x0)))
new_primCmpInt(Pos(Zero), Neg(Succ(x0)))
new_lt19(x0, x1, x2, x3)
new_esEs25(x0, x1, ty_Double)
new_lt6(x0, x1, ty_Ordering)
new_esEs17([], [], x0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs4(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs11(True, True)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_lt5(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs19(x0, x1, app(ty_[], x2))
new_ltEs7(Left(x0), Left(x1), ty_Char, x2)
new_ltEs5(x0, x1)
new_compare14(x0, x1, False, x2, x3)
new_ltEs7(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare23(x0, x1, True, x2, x3)
new_primCmpNat0(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Integer)
new_esEs12(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs14(Char(x0), Char(x1))
new_compare8(x0, x1)
new_lt6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare32(x0, x1, app(ty_Maybe, x2))
new_compare7(Float(x0, x1), Float(x2, x3))
new_esEs12(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs6(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs9(EQ)
new_lt20(x0, x1, app(app(ty_@2, x2), x3))
new_compare32(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs5(Just(x0), Nothing, x1)
new_esEs4(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs10(x0, x1)
new_esEs12(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Int)
new_compare32(x0, x1, ty_Int)
new_esEs5(Nothing, Nothing, x0)
new_compare32(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_lt8(x0, x1, x2)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_ltEs7(Right(x0), Right(x1), x2, ty_Double)
new_esEs22(x0, x1, ty_@0)
new_compare32(x0, x1, ty_Float)
new_ltEs7(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs7(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_compare31(x0, x1, x2, x3)
new_compare110(x0, x1, True, x2)
new_esEs11(False, True)
new_esEs11(True, False)
new_ltEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, ty_@0)
new_ltEs6(Just(x0), Just(x1), ty_Ordering)
new_compare14(x0, x1, True, x2, x3)
new_compare32(x0, x1, app(ty_Ratio, x2))
new_lt20(x0, x1, ty_Float)
new_primMulInt(Pos(x0), Neg(x1))
new_primMulInt(Neg(x0), Pos(x1))
new_compare19(Char(x0), Char(x1))
new_ltEs19(x0, x1, app(ty_Ratio, x2))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs8(@0, @0)
new_esEs4(Left(x0), Right(x1), x2, x3)
new_esEs4(Right(x0), Left(x1), x2, x3)
new_esEs16(GT, LT)
new_esEs16(LT, GT)
new_primEqNat0(Zero, Succ(x0))
new_ltEs6(Just(x0), Just(x1), ty_Float)
new_esEs27(x0, x1, ty_Bool)
new_compare28(x0, x1, x2)
new_esEs22(x0, x1, ty_Double)
new_ltEs6(Just(x0), Just(x1), ty_Integer)
new_ltEs17(@2(x0, x1), @2(x2, x3), x4, x5)
new_lt4(x0, x1)
new_lt5(x0, x1, app(ty_Ratio, x2))
new_lt5(x0, x1, app(ty_[], x2))
new_compare9(x0, x1)
new_ltEs7(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_lt5(x0, x1, ty_Ordering)
new_lt18(x0, x1)
new_ltEs19(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Int)
new_primCmpInt(Neg(Succ(x0)), Neg(x1))
new_lt6(x0, x1, ty_Float)
new_ltEs7(Right(x0), Right(x1), x2, ty_Int)
new_ltEs7(Right(x0), Left(x1), x2, x3)
new_ltEs7(Left(x0), Right(x1), x2, x3)
new_compare23(x0, x1, False, x2, x3)
new_compare16(Double(x0, x1), Double(x2, x3))
new_ltEs18(x0, x1, ty_Float)
new_ltEs6(Just(x0), Just(x1), ty_Int)
new_primMulInt(Neg(x0), Neg(x1))
new_primMulNat0(Succ(x0), Zero)
new_ltEs18(x0, x1, ty_Char)
new_esEs22(x0, x1, ty_Bool)
new_lt20(x0, x1, ty_Char)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_compare30(x0, x1, x2, x3, x4)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_lt20(x0, x1, ty_Double)
new_ltEs7(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs4(Right(x0), Right(x1), x2, ty_Integer)
new_compare29(x0, x1, x2, x3)
new_ltEs14(EQ, EQ)
new_primEqNat0(Zero, Zero)
new_lt6(x0, x1, ty_Bool)
new_ltEs7(Right(x0), Right(x1), x2, ty_Float)
new_lt6(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs12(x0, x1, ty_Bool)
new_ltEs16(x0, x1)
new_ltEs6(Just(x0), Just(x1), ty_Double)
new_compare12(@0, @0)
new_esEs5(Just(x0), Just(x1), ty_Ordering)
new_ltEs19(x0, x1, ty_Char)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_primCompAux00(x0, GT)
new_compare11(x0, x1, True)
new_primMulNat0(Zero, Zero)
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_ltEs6(Just(x0), Just(x1), ty_@0)
new_esEs12(x0, x1, app(ty_Ratio, x2))
new_esEs4(Right(x0), Right(x1), x2, ty_Float)
new_sr(Integer(x0), Integer(x1))
new_ltEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_lt6(x0, x1, ty_Int)
new_esEs5(Just(x0), Just(x1), ty_Double)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs20(x0, x1, ty_@0)
new_lt5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs7(Left(x0), Left(x1), ty_Integer, x2)
new_ltEs7(Left(x0), Left(x1), ty_@0, x2)
new_esEs5(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_ltEs7(Right(x0), Right(x1), x2, ty_Char)
new_esEs12(x0, x1, ty_Char)
new_esEs16(GT, GT)
new_esEs21(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_lt11(x0, x1, x2)
new_compare18(:%(x0, x1), :%(x2, x3), ty_Int)
new_ltEs18(x0, x1, ty_Ordering)
new_compare15(x0, x1, False, x2, x3)
new_esEs13(Float(x0, x1), Float(x2, x3))
new_esEs5(Just(x0), Just(x1), ty_Integer)
new_primEqNat0(Succ(x0), Zero)
new_primCmpInt(Neg(Succ(x0)), Pos(x1))
new_primCmpInt(Pos(Succ(x0)), Neg(x1))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Char)
new_ltEs18(x0, x1, app(ty_Maybe, x2))
new_esEs4(Left(x0), Left(x1), app(ty_[], x2), x3)
new_lt9(x0, x1)
new_asAs(False, x0)
new_esEs4(Left(x0), Left(x1), ty_Integer, x2)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_lt5(x0, x1, ty_Integer)
new_ltEs6(Just(x0), Nothing, x1)
new_esEs26(x0, x1, ty_Int)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(False, False)
new_ltEs12(False, False)
new_compare25(x0, x1, True, x2, x3)
new_esEs21(x0, x1, ty_Float)
new_primMulInt(Pos(x0), Pos(x1))
new_compare13(x0, x1, True, x2, x3, x4)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Char)
new_primCompAux0(x0, x1, x2, x3)
new_ltEs19(x0, x1, ty_Bool)
new_compare15(x0, x1, True, x2, x3)
new_esEs4(Right(x0), Right(x1), x2, ty_Char)
new_ltEs19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Char)
new_compare25(x0, x1, False, x2, x3)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Double)
new_primMulNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_primPlusNat1(Zero, Zero)
new_not0
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs12(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(Just(x0), Just(x1), app(ty_[], x2))
new_ltEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_lt20(x0, x1, ty_Int)
new_compare6(Integer(x0), Integer(x1))
new_ltEs7(Left(x0), Left(x1), app(ty_[], x2), x3)
new_ltEs8(x0, x1)
new_esEs9(GT)
new_ltEs14(LT, LT)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_@0)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt14(x0, x1)
new_primCmpInt(Neg(Zero), Neg(Zero))
new_ltEs4(x0, x1, x2)
new_esEs25(x0, x1, ty_@0)
new_primCompAux00(x0, LT)
new_esEs21(x0, x1, app(ty_[], x2))
new_compare4([], [], x0)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(Left(x0), Left(x1), ty_Float, x2)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs5(Just(x0), Just(x1), ty_@0)
new_lt13(x0, x1)
new_esEs4(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_asAs(True, x0)
new_ltEs7(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_lt6(x0, x1, ty_Char)
new_lt5(x0, x1, app(ty_Maybe, x2))
new_compare210(x0, x1, True, x2)
new_primCmpNat0(Zero, Succ(x0))
new_esEs26(x0, x1, ty_Double)
new_ltEs6(Nothing, Just(x0), x1)
new_not(GT)
new_compare32(x0, x1, ty_Ordering)
new_esEs4(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_ltEs10(x0, x1, x2)
new_lt5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Bool)
new_ltEs7(Right(x0), Right(x1), x2, ty_Bool)
new_compare17(x0, x1)
new_lt20(x0, x1, app(ty_[], x2))
new_ltEs7(Right(x0), Right(x1), x2, ty_Integer)
new_esEs20(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs5(Just(x0), Just(x1), app(ty_Maybe, x2))
new_lt20(x0, x1, ty_Ordering)
new_ltEs14(EQ, LT)
new_ltEs14(LT, EQ)
new_esEs5(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(Left(x0), Left(x1), ty_Int, x2)
new_lt5(x0, x1, ty_@0)
new_compare210(x0, x1, False, x2)
new_esEs7(@2(x0, x1), @2(x2, x3), x4, x5)
new_compare32(x0, x1, ty_Bool)
new_compare27(x0, x1, False)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_lt5(x0, x1, ty_Char)
new_primCmpInt(Pos(Zero), Pos(Zero))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt7(x0, x1, x2, x3)
new_compare32(x0, x1, app(app(ty_@2, x2), x3))
new_compare13(x0, x1, False, x2, x3, x4)
new_ltEs19(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs4(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_lt6(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Float)
new_esEs4(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs26(x0, x1, ty_Ordering)
new_esEs4(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_ltEs18(x0, x1, ty_@0)
new_esEs16(LT, LT)
new_lt5(x0, x1, ty_Float)
new_ltEs18(x0, x1, ty_Double)
new_esEs12(x0, x1, app(app(ty_@2, x2), x3))
new_compare32(x0, x1, ty_@0)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs4(Right(x0), Right(x1), x2, ty_Bool)
new_ltEs7(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs25(x0, x1, ty_Ordering)
new_ltEs7(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_lt6(x0, x1, ty_Integer)
new_compare32(x0, x1, app(ty_[], x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_compare4([], :(x0, x1), x2)
new_ltEs18(x0, x1, app(app(ty_@2, x2), x3))
new_lt12(x0, x1)
new_esEs12(x0, x1, ty_Int)
new_lt20(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_@0)
new_ltEs19(x0, x1, ty_Float)
new_esEs5(Just(x0), Just(x1), ty_Int)
new_compare26(x0, x1, False)
new_esEs27(x0, x1, ty_Int)
new_esEs15(Integer(x0), Integer(x1))
new_primPlusNat0(Zero, x0)
new_esEs12(x0, x1, app(ty_[], x2))
new_esEs9(LT)
new_compare110(x0, x1, False, x2)
new_ltEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs4(Left(x0), Left(x1), ty_Char, x2)
new_ltEs19(x0, x1, app(ty_Maybe, x2))
new_compare27(x0, x1, True)
new_ltEs12(True, False)
new_ltEs12(False, True)
new_esEs24(x0, x1, ty_Integer)
new_esEs4(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_lt20(x0, x1, ty_@0)
new_esEs20(x0, x1, ty_Float)
new_esEs21(x0, x1, ty_Double)
new_ltEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs14(EQ, GT)
new_ltEs14(GT, EQ)
new_esEs4(Right(x0), Right(x1), x2, ty_Double)
new_ltEs6(Just(x0), Just(x1), app(ty_[], x2))
new_ltEs7(Left(x0), Left(x1), ty_Bool, x2)
new_primCmpNat0(Zero, Zero)
new_ltEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_lt20(x0, x1, ty_Bool)
new_compare11(x0, x1, False)
new_ltEs18(x0, x1, app(ty_[], x2))
new_esEs5(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_ltEs15(x0, x1)
new_ltEs7(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_ltEs7(Left(x0), Left(x1), ty_Float, x2)
new_ltEs7(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_pePe(False, x0, x1, x2, x3)
new_ltEs7(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs26(x0, x1, ty_Char)
new_lt20(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Int)
new_esEs4(Right(x0), Right(x1), x2, ty_@0)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Integer)
new_ltEs7(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_esEs12(x0, x1, ty_Ordering)
new_ltEs14(GT, LT)
new_ltEs14(LT, GT)
new_ltEs18(x0, x1, ty_Integer)
new_esEs5(Nothing, Just(x0), x1)
new_primCmpInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Ordering)
new_compare26(x0, x1, True)
new_ltEs6(Just(x0), Just(x1), ty_Char)
new_primCmpInt(Pos(Succ(x0)), Pos(x1))
new_esEs26(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Float)
new_compare24(x0, x1, False, x2, x3, x4)
new_ltEs7(Left(x0), Left(x1), ty_Int, x2)
new_ltEs18(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(Right(x0), Right(x1), x2, ty_Int)
new_ltEs14(GT, GT)
new_ltEs18(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Float)
new_compare32(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_ltEs19(x0, x1, ty_@0)
new_esEs12(x0, x1, ty_@0)
new_esEs5(Just(x0), Just(x1), ty_Bool)
new_esEs4(Left(x0), Left(x1), ty_Double, x2)
new_esEs12(x0, x1, ty_Double)
new_not(EQ)
new_lt6(x0, x1, ty_Double)
new_compare4(:(x0, x1), [], x2)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(LT, EQ)
new_esEs16(EQ, LT)
new_ltEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_ltEs6(Nothing, Nothing, x0)
new_esEs16(EQ, EQ)
new_primCmpInt(Neg(Zero), Pos(Zero))
new_primCmpInt(Pos(Zero), Neg(Zero))
new_ltEs19(x0, x1, ty_Integer)
new_lt20(x0, x1, app(app(ty_Either, x2), x3))
new_compare10(x0, x1, True)
new_ltEs18(x0, x1, ty_Int)
new_esEs4(Right(x0), Right(x1), x2, app(ty_[], x3))
new_compare10(x0, x1, False)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs27(x0, x1, ty_Integer)
new_ltEs6(Just(x0), Just(x1), ty_Bool)
new_ltEs12(True, True)
new_esEs4(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_lt15(x0, x1)
new_lt5(x0, x1, ty_Int)
new_lt10(x0, x1, x2, x3, x4)
new_esEs25(x0, x1, ty_Bool)
new_lt5(x0, x1, ty_Bool)
new_ltEs7(Right(x0), Right(x1), x2, ty_@0)
new_lt16(x0, x1, x2)
new_ltEs7(Right(x0), Right(x1), x2, ty_Ordering)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpInt(Pos(Zero), Pos(Succ(x0)))
new_ltEs18(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Double)
new_esEs17(:(x0, x1), [], x2)
new_esEs16(GT, EQ)
new_esEs16(EQ, GT)
new_lt6(x0, x1, ty_@0)
new_lt20(x0, x1, ty_Integer)
new_compare32(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_Int)
new_ltEs9(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs5(Just(x0), Just(x1), ty_Char)
new_compare32(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(x0, x1, ty_Float)
new_ltEs7(Left(x0), Left(x1), ty_Ordering, x2)
new_primPlusNat1(Succ(x0), Succ(x1))
new_lt6(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt17(x0, x1)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Float)
new_ltEs19(x0, x1, ty_Int)
new_primCompAux00(x0, EQ)
new_pePe(True, x0, x1, x2, x3)
new_esEs4(Left(x0), Left(x1), ty_Bool, x2)
new_lt6(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Ordering)
new_esEs20(x0, x1, ty_Int)
new_compare4(:(x0, x1), :(x2, x3), x4)
new_ltEs11(x0, x1)
new_esEs21(x0, x1, ty_Ordering)
new_ltEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat0(Succ(x0), x1)
new_primEqInt(Pos(Zero), Pos(Zero))
new_sr0(x0, x1)
new_esEs20(x0, x1, ty_Bool)
new_compare24(x0, x1, True, x2, x3, x4)
new_esEs25(x0, x1, ty_Char)
new_lt6(x0, x1, app(app(ty_Either, x2), x3))
new_primCmpNat0(Succ(x0), Succ(x1))
new_ltEs13(x0, x1)
new_lt5(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_Integer)
new_compare18(:%(x0, x1), :%(x2, x3), ty_Integer)
new_not(LT)
new_esEs4(Left(x0), Left(x1), ty_@0, x2)
new_esEs4(Left(x0), Left(x1), app(ty_Maybe, x2), x3)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldl(vwx30, :(vwx310, vwx311), ba) → new_foldl(new_min1(vwx30, vwx310, ba), vwx311, ba)

The TRS R consists of the following rules:

new_esEs26(vwx200, vwx210, ty_Char) → new_esEs14(vwx200, vwx210)
new_esEs16(GT, EQ) → False
new_esEs16(EQ, GT) → False
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Ordering, cch) → new_ltEs14(vwx3000, vwx31000)
new_min1(Nothing, Nothing, ba) → Nothing
new_esEs20(vwx202, vwx212, ty_Ordering) → new_esEs16(vwx202, vwx212)
new_lt6(vwx3001, vwx31001, app(app(app(ty_@3, eg), eh), fa)) → new_lt10(vwx3001, vwx31001, eg, eh, fa)
new_esEs20(vwx202, vwx212, ty_Double) → new_esEs19(vwx202, vwx212)
new_compare15(vwx3000, vwx31000, True, db, dc) → LT
new_esEs20(vwx202, vwx212, ty_@0) → new_esEs8(vwx202, vwx212)
new_ltEs14(GT, GT) → True
new_esEs27(vwx200, vwx210, app(ty_Ratio, dbh)) → new_esEs18(vwx200, vwx210, dbh)
new_esEs4(Right(vwx200), Right(vwx210), bab, app(app(app(ty_@3, cab), cac), cad)) → new_esEs6(vwx200, vwx210, cab, cac, cad)
new_ltEs20(vwx300, vwx3100, ty_@0) → new_ltEs8(vwx300, vwx3100)
new_lt20(vwx3000, vwx31000, ty_Float) → new_lt14(vwx3000, vwx31000)
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Float, cch) → new_ltEs5(vwx3000, vwx31000)
new_ltEs6(Nothing, Just(vwx31000), bc) → True
new_ltEs7(Left(vwx3000), Left(vwx31000), app(app(ty_@2, cea), ceb), cch) → new_ltEs17(vwx3000, vwx31000, cea, ceb)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Char) → new_ltEs16(vwx3000, vwx31000)
new_esEs4(Right(vwx200), Right(vwx210), bab, app(ty_Maybe, cag)) → new_esEs5(vwx200, vwx210, cag)
new_esEs4(Left(vwx200), Left(vwx210), ty_Double, bac) → new_esEs19(vwx200, vwx210)
new_lt17(vwx3000, vwx31000) → new_esEs9(new_compare16(vwx3000, vwx31000))
new_esEs26(vwx200, vwx210, ty_Float) → new_esEs13(vwx200, vwx210)
new_ltEs7(Left(vwx3000), Right(vwx31000), ccg, cch) → True
new_primMulNat0(Zero, Zero) → Zero
new_compare13(vwx3000, vwx31000, False, de, df, dg) → GT
new_primCompAux0(vwx3000, vwx31000, vwx47, bb) → new_primCompAux00(vwx47, new_compare32(vwx3000, vwx31000, bb))
new_sr(Integer(vwx30000), Integer(vwx310010)) → Integer(new_primMulInt(vwx30000, vwx310010))
new_lt8(vwx3000, vwx31000, dd) → new_esEs9(new_compare28(vwx3000, vwx31000, dd))
new_lt4(vwx3000, vwx31000) → new_esEs9(new_compare9(vwx3000, vwx31000))
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_@0, cch) → new_ltEs8(vwx3000, vwx31000)
new_esEs4(Right(vwx200), Right(vwx210), bab, app(ty_Ratio, caf)) → new_esEs18(vwx200, vwx210, caf)
new_ltEs18(vwx3002, vwx31002, ty_Char) → new_ltEs16(vwx3002, vwx31002)
new_esEs9(LT) → True
new_esEs24(vwx200, vwx210, ty_Integer) → new_esEs15(vwx200, vwx210)
new_esEs25(vwx201, vwx211, app(ty_Ratio, cga)) → new_esEs18(vwx201, vwx211, cga)
new_lt5(vwx3000, vwx31000, app(app(ty_Either, db), dc)) → new_lt7(vwx3000, vwx31000, db, dc)
new_esEs4(Right(vwx200), Right(vwx210), bab, ty_Bool) → new_esEs11(vwx200, vwx210)
new_not(GT) → False
new_esEs20(vwx202, vwx212, app(app(ty_Either, beb), bec)) → new_esEs4(vwx202, vwx212, beb, bec)
new_esEs4(Right(vwx200), Right(vwx210), bab, ty_Int) → new_esEs10(vwx200, vwx210)
new_ltEs13(vwx300, vwx3100) → new_not(new_compare8(vwx300, vwx3100))
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Int) → new_ltEs13(vwx3000, vwx31000)
new_lt6(vwx3001, vwx31001, app(app(ty_@2, fd), ff)) → new_lt19(vwx3001, vwx31001, fd, ff)
new_ltEs20(vwx300, vwx3100, app(app(ty_@2, bad), bae)) → new_ltEs17(vwx300, vwx3100, bad, bae)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Ordering) → new_ltEs14(vwx3000, vwx31000)
new_esEs5(Just(vwx200), Just(vwx210), app(ty_Maybe, cca)) → new_esEs5(vwx200, vwx210, cca)
new_esEs15(Integer(vwx200), Integer(vwx210)) → new_primEqInt(vwx200, vwx210)
new_min10(vwx8, vwx9, True, dbc) → Just(vwx8)
new_ltEs18(vwx3002, vwx31002, ty_Float) → new_ltEs5(vwx3002, vwx31002)
new_esEs22(vwx200, vwx210, app(ty_Ratio, bgb)) → new_esEs18(vwx200, vwx210, bgb)
new_esEs19(Double(vwx200, vwx201), Double(vwx210, vwx211)) → new_esEs10(new_sr0(vwx200, vwx210), new_sr0(vwx201, vwx211))
new_ltEs6(Just(vwx3000), Just(vwx31000), app(ty_Ratio, cb)) → new_ltEs10(vwx3000, vwx31000, cb)
new_ltEs7(Left(vwx3000), Left(vwx31000), app(app(app(ty_@3, cdd), cde), cdf), cch) → new_ltEs9(vwx3000, vwx31000, cdd, cde, cdf)
new_esEs25(vwx201, vwx211, ty_Float) → new_esEs13(vwx201, vwx211)
new_esEs25(vwx201, vwx211, app(app(ty_@2, cgc), cgd)) → new_esEs7(vwx201, vwx211, cgc, cgd)
new_esEs25(vwx201, vwx211, app(app(ty_Either, cge), cgf)) → new_esEs4(vwx201, vwx211, cge, cgf)
new_ltEs12(True, False) → False
new_esEs22(vwx200, vwx210, app(app(ty_Either, bgf), bgg)) → new_esEs4(vwx200, vwx210, bgf, bgg)
new_ltEs14(GT, EQ) → False
new_lt5(vwx3000, vwx31000, app(ty_[], ea)) → new_lt16(vwx3000, vwx31000, ea)
new_ltEs6(Just(vwx3000), Just(vwx31000), app(app(app(ty_@3, bg), bh), ca)) → new_ltEs9(vwx3000, vwx31000, bg, bh, ca)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, ty_Bool) → new_ltEs12(vwx3000, vwx31000)
new_compare18(:%(vwx3000, vwx3001), :%(vwx31000, vwx31001), ty_Integer) → new_compare6(new_sr(vwx3000, vwx31001), new_sr(vwx31000, vwx3001))
new_esEs12(vwx20, vwx21, app(ty_[], he)) → new_esEs17(vwx20, vwx21, he)
new_lt20(vwx3000, vwx31000, app(app(app(ty_@3, bba), bbb), bbc)) → new_lt10(vwx3000, vwx31000, bba, bbb, bbc)
new_compare7(Float(vwx3000, vwx3001), Float(vwx31000, vwx31001)) → new_compare8(new_sr0(vwx3000, vwx31000), new_sr0(vwx3001, vwx31001))
new_esEs7(@2(vwx200, vwx201), @2(vwx210, vwx211), hh, baa) → new_asAs(new_esEs26(vwx200, vwx210, hh), new_esEs25(vwx201, vwx211, baa))
new_lt5(vwx3000, vwx31000, app(app(app(ty_@3, de), df), dg)) → new_lt10(vwx3000, vwx31000, de, df, dg)
new_esEs27(vwx200, vwx210, ty_Ordering) → new_esEs16(vwx200, vwx210)
new_esEs27(vwx200, vwx210, app(ty_[], dbg)) → new_esEs17(vwx200, vwx210, dbg)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, ty_Char) → new_ltEs16(vwx3000, vwx31000)
new_esEs5(Just(vwx200), Just(vwx210), ty_Integer) → new_esEs15(vwx200, vwx210)
new_lt11(vwx3000, vwx31000, dh) → new_esEs9(new_compare18(vwx3000, vwx31000, dh))
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, ty_Int) → new_ltEs13(vwx3000, vwx31000)
new_esEs4(Right(vwx200), Right(vwx210), bab, ty_Integer) → new_esEs15(vwx200, vwx210)
new_compare9(vwx3000, vwx31000) → new_compare26(vwx3000, vwx31000, new_esEs16(vwx3000, vwx31000))
new_lt5(vwx3000, vwx31000, ty_Int) → new_lt15(vwx3000, vwx31000)
new_esEs21(vwx201, vwx211, ty_@0) → new_esEs8(vwx201, vwx211)
new_lt6(vwx3001, vwx31001, ty_@0) → new_lt9(vwx3001, vwx31001)
new_ltEs18(vwx3002, vwx31002, ty_Int) → new_ltEs13(vwx3002, vwx31002)
new_lt20(vwx3000, vwx31000, app(app(ty_Either, baf), bag)) → new_lt7(vwx3000, vwx31000, baf, bag)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, ty_Float) → new_ltEs5(vwx3000, vwx31000)
new_primCmpNat0(Zero, Succ(vwx310000)) → LT
new_esEs4(Right(vwx200), Right(vwx210), bab, app(app(ty_@2, cah), cba)) → new_esEs7(vwx200, vwx210, cah, cba)
new_esEs21(vwx201, vwx211, ty_Double) → new_esEs19(vwx201, vwx211)
new_esEs26(vwx200, vwx210, ty_Bool) → new_esEs11(vwx200, vwx210)
new_ltEs6(Just(vwx3000), Just(vwx31000), app(app(ty_@2, cd), ce)) → new_ltEs17(vwx3000, vwx31000, cd, ce)
new_lt6(vwx3001, vwx31001, ty_Char) → new_lt18(vwx3001, vwx31001)
new_ltEs6(Just(vwx3000), Just(vwx31000), app(app(ty_Either, bd), be)) → new_ltEs7(vwx3000, vwx31000, bd, be)
new_lt5(vwx3000, vwx31000, ty_Ordering) → new_lt4(vwx3000, vwx31000)
new_esEs25(vwx201, vwx211, ty_Char) → new_esEs14(vwx201, vwx211)
new_esEs20(vwx202, vwx212, ty_Bool) → new_esEs11(vwx202, vwx212)
new_ltEs15(vwx300, vwx3100) → new_not(new_compare16(vwx300, vwx3100))
new_esEs4(Right(vwx200), Right(vwx210), bab, ty_Char) → new_esEs14(vwx200, vwx210)
new_lt20(vwx3000, vwx31000, app(app(ty_@2, bbf), bbg)) → new_lt19(vwx3000, vwx31000, bbf, bbg)
new_esEs20(vwx202, vwx212, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs6(vwx202, vwx212, bdb, bdc, bdd)
new_esEs5(Just(vwx200), Just(vwx210), app(ty_[], cbg)) → new_esEs17(vwx200, vwx210, cbg)
new_primEqNat0(Zero, Zero) → True
new_compare14(vwx3000, vwx31000, False, eb, ec) → GT
new_ltEs9(@3(vwx3000, vwx3001, vwx3002), @3(vwx31000, vwx31001, vwx31002), cf, cg, da) → new_pePe(new_lt5(vwx3000, vwx31000, cf), vwx3000, vwx31000, new_pePe(new_lt6(vwx3001, vwx31001, cg), vwx3001, vwx31001, new_ltEs18(vwx3002, vwx31002, da), cg), cf)
new_ltEs19(vwx3001, vwx31001, ty_Int) → new_ltEs13(vwx3001, vwx31001)
new_compare26(vwx3000, vwx31000, True) → EQ
new_ltEs12(False, False) → True
new_lt20(vwx3000, vwx31000, ty_Int) → new_lt15(vwx3000, vwx31000)
new_esEs16(GT, LT) → False
new_esEs16(LT, GT) → False
new_ltEs19(vwx3001, vwx31001, app(ty_[], bcg)) → new_ltEs4(vwx3001, vwx31001, bcg)
new_compare27(vwx3000, vwx31000, False) → new_compare11(vwx3000, vwx31000, new_ltEs12(vwx3000, vwx31000))
new_esEs22(vwx200, vwx210, app(app(ty_@2, bgd), bge)) → new_esEs7(vwx200, vwx210, bgd, bge)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_@0) → new_ltEs8(vwx3000, vwx31000)
new_ltEs11(vwx300, vwx3100) → new_not(new_compare6(vwx300, vwx3100))
new_esEs5(Just(vwx200), Just(vwx210), ty_Ordering) → new_esEs16(vwx200, vwx210)
new_ltEs17(@2(vwx3000, vwx3001), @2(vwx31000, vwx31001), bad, bae) → new_pePe(new_lt20(vwx3000, vwx31000, bad), vwx3000, vwx31000, new_ltEs19(vwx3001, vwx31001, bae), bad)
new_compare32(vwx3000, vwx31000, app(app(ty_@2, dba), dbb)) → new_compare29(vwx3000, vwx31000, dba, dbb)
new_esEs12(vwx20, vwx21, app(app(ty_@2, hh), baa)) → new_esEs7(vwx20, vwx21, hh, baa)
new_ltEs14(EQ, LT) → False
new_esEs4(Left(vwx200), Left(vwx210), app(ty_[], bhc), bac) → new_esEs17(vwx200, vwx210, bhc)
new_ltEs18(vwx3002, vwx31002, app(app(app(ty_@3, gb), gc), gd)) → new_ltEs9(vwx3002, vwx31002, gb, gc, gd)
new_compare4([], [], bb) → EQ
new_primPlusNat0(Succ(vwx650), vwx3100100) → Succ(Succ(new_primPlusNat1(vwx650, vwx3100100)))
new_compare29(vwx3000, vwx31000, eb, ec) → new_compare23(vwx3000, vwx31000, new_esEs7(vwx3000, vwx31000, eb, ec), eb, ec)
new_esEs4(Right(vwx200), Right(vwx210), bab, ty_@0) → new_esEs8(vwx200, vwx210)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Integer) → new_ltEs11(vwx3000, vwx31000)
new_lt20(vwx3000, vwx31000, ty_Double) → new_lt17(vwx3000, vwx31000)
new_esEs26(vwx200, vwx210, app(app(app(ty_@3, cgg), cgh), cha)) → new_esEs6(vwx200, vwx210, cgg, cgh, cha)
new_ltEs19(vwx3001, vwx31001, ty_Bool) → new_ltEs12(vwx3001, vwx31001)
new_lt12(vwx3000, vwx31000) → new_esEs9(new_compare6(vwx3000, vwx31000))
new_esEs4(Right(vwx200), Right(vwx210), bab, app(app(ty_Either, cbb), cbc)) → new_esEs4(vwx200, vwx210, cbb, cbc)
new_esEs22(vwx200, vwx210, ty_Char) → new_esEs14(vwx200, vwx210)
new_compare24(vwx3000, vwx31000, True, de, df, dg) → EQ
new_primEqInt(Neg(Succ(vwx2000)), Neg(Succ(vwx2100))) → new_primEqNat0(vwx2000, vwx2100)
new_ltEs20(vwx300, vwx3100, ty_Integer) → new_ltEs11(vwx300, vwx3100)
new_ltEs19(vwx3001, vwx31001, app(app(ty_@2, bch), bda)) → new_ltEs17(vwx3001, vwx31001, bch, bda)
new_lt20(vwx3000, vwx31000, app(ty_Ratio, bbd)) → new_lt11(vwx3000, vwx31000, bbd)
new_ltEs18(vwx3002, vwx31002, app(ty_Ratio, ge)) → new_ltEs10(vwx3002, vwx31002, ge)
new_esEs25(vwx201, vwx211, ty_Bool) → new_esEs11(vwx201, vwx211)
new_esEs4(Right(vwx200), Right(vwx210), bab, app(ty_[], cae)) → new_esEs17(vwx200, vwx210, cae)
new_esEs9(GT) → False
new_esEs22(vwx200, vwx210, app(app(app(ty_@3, bff), bfg), bfh)) → new_esEs6(vwx200, vwx210, bff, bfg, bfh)
new_lt16(vwx3000, vwx31000, ea) → new_esEs9(new_compare4(vwx3000, vwx31000, ea))
new_min1(Just(vwx300), Just(vwx3100), ba) → new_min10(vwx300, vwx3100, new_ltEs20(vwx300, vwx3100, ba), ba)
new_ltEs18(vwx3002, vwx31002, app(app(ty_Either, fg), fh)) → new_ltEs7(vwx3002, vwx31002, fg, fh)
new_esEs4(Left(vwx200), Left(vwx210), app(app(ty_Either, bhh), caa), bac) → new_esEs4(vwx200, vwx210, bhh, caa)
new_ltEs19(vwx3001, vwx31001, app(app(app(ty_@3, bcc), bcd), bce)) → new_ltEs9(vwx3001, vwx31001, bcc, bcd, bce)
new_ltEs20(vwx300, vwx3100, app(app(app(ty_@3, cf), cg), da)) → new_ltEs9(vwx300, vwx3100, cf, cg, da)
new_primPlusNat1(Zero, Succ(vwx31001000)) → Succ(vwx31001000)
new_primPlusNat1(Succ(vwx6500), Zero) → Succ(vwx6500)
new_ltEs20(vwx300, vwx3100, ty_Bool) → new_ltEs12(vwx300, vwx3100)
new_esEs6(@3(vwx200, vwx201, vwx202), @3(vwx210, vwx211, vwx212), hb, hc, hd) → new_asAs(new_esEs22(vwx200, vwx210, hb), new_asAs(new_esEs21(vwx201, vwx211, hc), new_esEs20(vwx202, vwx212, hd)))
new_lt5(vwx3000, vwx31000, ty_Integer) → new_lt12(vwx3000, vwx31000)
new_esEs9(EQ) → False
new_esEs4(Left(vwx200), Left(vwx210), ty_Int, bac) → new_esEs10(vwx200, vwx210)
new_lt6(vwx3001, vwx31001, ty_Bool) → new_lt13(vwx3001, vwx31001)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_ltEs7(Right(vwx3000), Left(vwx31000), ccg, cch) → False
new_esEs5(Just(vwx200), Just(vwx210), ty_Int) → new_esEs10(vwx200, vwx210)
new_lt6(vwx3001, vwx31001, ty_Ordering) → new_lt4(vwx3001, vwx31001)
new_ltEs5(vwx300, vwx3100) → new_not(new_compare7(vwx300, vwx3100))
new_lt6(vwx3001, vwx31001, app(ty_Ratio, fb)) → new_lt11(vwx3001, vwx31001, fb)
new_esEs21(vwx201, vwx211, app(app(ty_@2, bfb), bfc)) → new_esEs7(vwx201, vwx211, bfb, bfc)
new_esEs20(vwx202, vwx212, ty_Float) → new_esEs13(vwx202, vwx212)
new_compare8(vwx300, vwx3100) → new_primCmpInt(vwx300, vwx3100)
new_ltEs20(vwx300, vwx3100, app(ty_[], bb)) → new_ltEs4(vwx300, vwx3100, bb)
new_primEqInt(Neg(Zero), Neg(Succ(vwx2100))) → False
new_primEqInt(Neg(Succ(vwx2000)), Neg(Zero)) → False
new_lt18(vwx3000, vwx31000) → new_esEs9(new_compare19(vwx3000, vwx31000))
new_lt5(vwx3000, vwx31000, ty_@0) → new_lt9(vwx3000, vwx31000)
new_lt6(vwx3001, vwx31001, app(ty_Maybe, ef)) → new_lt8(vwx3001, vwx31001, ef)
new_esEs22(vwx200, vwx210, ty_Float) → new_esEs13(vwx200, vwx210)
new_esEs21(vwx201, vwx211, app(app(ty_Either, bfd), bfe)) → new_esEs4(vwx201, vwx211, bfd, bfe)
new_esEs21(vwx201, vwx211, ty_Ordering) → new_esEs16(vwx201, vwx211)
new_compare32(vwx3000, vwx31000, ty_Double) → new_compare16(vwx3000, vwx31000)
new_primCmpInt(Neg(Zero), Pos(Zero)) → EQ
new_primCmpInt(Pos(Zero), Neg(Zero)) → EQ
new_compare210(vwx3000, vwx31000, False, dd) → new_compare110(vwx3000, vwx31000, new_ltEs6(vwx3000, vwx31000, dd), dd)
new_ltEs20(vwx300, vwx3100, ty_Double) → new_ltEs15(vwx300, vwx3100)
new_ltEs18(vwx3002, vwx31002, ty_@0) → new_ltEs8(vwx3002, vwx31002)
new_primCmpNat0(Succ(vwx30000), Succ(vwx310000)) → new_primCmpNat0(vwx30000, vwx310000)
new_esEs11(False, False) → True
new_primEqInt(Pos(Succ(vwx2000)), Pos(Succ(vwx2100))) → new_primEqNat0(vwx2000, vwx2100)
new_esEs25(vwx201, vwx211, app(ty_Maybe, cgb)) → new_esEs5(vwx201, vwx211, cgb)
new_esEs20(vwx202, vwx212, ty_Int) → new_esEs10(vwx202, vwx212)
new_esEs26(vwx200, vwx210, ty_Integer) → new_esEs15(vwx200, vwx210)
new_esEs22(vwx200, vwx210, ty_Double) → new_esEs19(vwx200, vwx210)
new_esEs5(Just(vwx200), Just(vwx210), ty_Bool) → new_esEs11(vwx200, vwx210)
new_ltEs19(vwx3001, vwx31001, app(ty_Ratio, bcf)) → new_ltEs10(vwx3001, vwx31001, bcf)
new_primEqNat0(Succ(vwx2000), Succ(vwx2100)) → new_primEqNat0(vwx2000, vwx2100)
new_esEs4(Left(vwx200), Left(vwx210), ty_Ordering, bac) → new_esEs16(vwx200, vwx210)
new_esEs12(vwx20, vwx21, ty_Float) → new_esEs13(vwx20, vwx21)
new_compare32(vwx3000, vwx31000, app(app(app(ty_@3, dad), dae), daf)) → new_compare30(vwx3000, vwx31000, dad, dae, daf)
new_min1(Just(vwx300), Nothing, ba) → Nothing
new_min1(Nothing, Just(vwx3100), ba) → Nothing
new_ltEs20(vwx300, vwx3100, ty_Char) → new_ltEs16(vwx300, vwx3100)
new_primCompAux00(vwx51, LT) → LT
new_primCmpInt(Neg(Succ(vwx30000)), Neg(vwx31000)) → new_primCmpNat0(vwx31000, Succ(vwx30000))
new_ltEs19(vwx3001, vwx31001, app(app(ty_Either, bbh), bca)) → new_ltEs7(vwx3001, vwx31001, bbh, bca)
new_esEs26(vwx200, vwx210, ty_@0) → new_esEs8(vwx200, vwx210)
new_lt19(vwx3000, vwx31000, eb, ec) → new_esEs9(new_compare29(vwx3000, vwx31000, eb, ec))
new_esEs12(vwx20, vwx21, app(app(ty_Either, bab), bac)) → new_esEs4(vwx20, vwx21, bab, bac)
new_esEs12(vwx20, vwx21, app(ty_Ratio, hf)) → new_esEs18(vwx20, vwx21, hf)
new_ltEs20(vwx300, vwx3100, ty_Ordering) → new_ltEs14(vwx300, vwx3100)
new_compare19(Char(vwx3000), Char(vwx31000)) → new_primCmpNat0(vwx3000, vwx31000)
new_primEqInt(Pos(Zero), Pos(Succ(vwx2100))) → False
new_primEqInt(Pos(Succ(vwx2000)), Pos(Zero)) → False
new_ltEs18(vwx3002, vwx31002, ty_Integer) → new_ltEs11(vwx3002, vwx31002)
new_ltEs19(vwx3001, vwx31001, app(ty_Maybe, bcb)) → new_ltEs6(vwx3001, vwx31001, bcb)
new_lt20(vwx3000, vwx31000, ty_Char) → new_lt18(vwx3000, vwx31000)
new_ltEs6(Just(vwx3000), Nothing, bc) → False
new_primCmpNat0(Zero, Zero) → EQ
new_primCmpNat0(Succ(vwx30000), Zero) → GT
new_compare31(vwx3000, vwx31000, db, dc) → new_compare25(vwx3000, vwx31000, new_esEs4(vwx3000, vwx31000, db, dc), db, dc)
new_primCmpInt(Neg(Zero), Pos(Succ(vwx310000))) → LT
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, ty_Double) → new_ltEs15(vwx3000, vwx31000)
new_ltEs6(Just(vwx3000), Just(vwx31000), app(ty_[], cc)) → new_ltEs4(vwx3000, vwx31000, cc)
new_primPlusNat1(Succ(vwx6500), Succ(vwx31001000)) → Succ(Succ(new_primPlusNat1(vwx6500, vwx31001000)))
new_compare6(Integer(vwx3000), Integer(vwx31000)) → new_primCmpInt(vwx3000, vwx31000)
new_primEqInt(Neg(Succ(vwx2000)), Pos(vwx210)) → False
new_primEqInt(Pos(Succ(vwx2000)), Neg(vwx210)) → False
new_esEs25(vwx201, vwx211, ty_Int) → new_esEs10(vwx201, vwx211)
new_compare210(vwx3000, vwx31000, True, dd) → EQ
new_esEs27(vwx200, vwx210, app(ty_Maybe, dca)) → new_esEs5(vwx200, vwx210, dca)
new_ltEs6(Just(vwx3000), Just(vwx31000), app(ty_Maybe, bf)) → new_ltEs6(vwx3000, vwx31000, bf)
new_esEs25(vwx201, vwx211, ty_@0) → new_esEs8(vwx201, vwx211)
new_primEqInt(Neg(Zero), Pos(Succ(vwx2100))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vwx2100))) → False
new_esEs26(vwx200, vwx210, ty_Int) → new_esEs10(vwx200, vwx210)
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Char, cch) → new_ltEs16(vwx3000, vwx31000)
new_esEs26(vwx200, vwx210, app(ty_[], chb)) → new_esEs17(vwx200, vwx210, chb)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, app(ty_[], cfb)) → new_ltEs4(vwx3000, vwx31000, cfb)
new_esEs21(vwx201, vwx211, ty_Integer) → new_esEs15(vwx201, vwx211)
new_primCmpInt(Pos(Zero), Pos(Succ(vwx310000))) → new_primCmpNat0(Zero, Succ(vwx310000))
new_primCompAux00(vwx51, EQ) → vwx51
new_esEs27(vwx200, vwx210, app(app(ty_@2, dcb), dcc)) → new_esEs7(vwx200, vwx210, dcb, dcc)
new_lt6(vwx3001, vwx31001, app(ty_[], fc)) → new_lt16(vwx3001, vwx31001, fc)
new_lt20(vwx3000, vwx31000, ty_Bool) → new_lt13(vwx3000, vwx31000)
new_lt20(vwx3000, vwx31000, ty_Ordering) → new_lt4(vwx3000, vwx31000)
new_ltEs20(vwx300, vwx3100, ty_Int) → new_ltEs13(vwx300, vwx3100)
new_esEs4(Right(vwx200), Right(vwx210), bab, ty_Ordering) → new_esEs16(vwx200, vwx210)
new_esEs22(vwx200, vwx210, ty_@0) → new_esEs8(vwx200, vwx210)
new_esEs4(Left(vwx200), Left(vwx210), ty_Integer, bac) → new_esEs15(vwx200, vwx210)
new_lt7(vwx3000, vwx31000, db, dc) → new_esEs9(new_compare31(vwx3000, vwx31000, db, dc))
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Int, cch) → new_ltEs13(vwx3000, vwx31000)
new_compare32(vwx3000, vwx31000, app(ty_Maybe, dac)) → new_compare28(vwx3000, vwx31000, dac)
new_pePe(False, vwx20, vwx21, vwx37, ha) → new_asAs(new_esEs12(vwx20, vwx21, ha), vwx37)
new_esEs21(vwx201, vwx211, app(ty_[], beg)) → new_esEs17(vwx201, vwx211, beg)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, app(ty_Ratio, cfa)) → new_ltEs10(vwx3000, vwx31000, cfa)
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Double, cch) → new_ltEs15(vwx3000, vwx31000)
new_ltEs20(vwx300, vwx3100, ty_Float) → new_ltEs5(vwx300, vwx3100)
new_compare12(@0, @0) → EQ
new_compare32(vwx3000, vwx31000, app(ty_[], dah)) → new_compare4(vwx3000, vwx31000, dah)
new_ltEs20(vwx300, vwx3100, app(ty_Ratio, ccf)) → new_ltEs10(vwx300, vwx3100, ccf)
new_primCmpInt(Pos(Succ(vwx30000)), Pos(vwx31000)) → new_primCmpNat0(Succ(vwx30000), vwx31000)
new_primPlusNat0(Zero, vwx3100100) → Succ(vwx3100100)
new_compare110(vwx3000, vwx31000, True, dd) → LT
new_esEs5(Just(vwx200), Just(vwx210), ty_Char) → new_esEs14(vwx200, vwx210)
new_compare32(vwx3000, vwx31000, ty_Char) → new_compare19(vwx3000, vwx31000)
new_ltEs7(Left(vwx3000), Left(vwx31000), app(ty_Ratio, cdg), cch) → new_ltEs10(vwx3000, vwx31000, cdg)
new_ltEs19(vwx3001, vwx31001, ty_Float) → new_ltEs5(vwx3001, vwx31001)
new_ltEs7(Left(vwx3000), Left(vwx31000), app(ty_Maybe, cdc), cch) → new_ltEs6(vwx3000, vwx31000, cdc)
new_esEs20(vwx202, vwx212, ty_Char) → new_esEs14(vwx202, vwx212)
new_esEs26(vwx200, vwx210, app(ty_Ratio, chc)) → new_esEs18(vwx200, vwx210, chc)
new_esEs25(vwx201, vwx211, ty_Integer) → new_esEs15(vwx201, vwx211)
new_esEs16(EQ, LT) → False
new_esEs16(LT, EQ) → False
new_ltEs18(vwx3002, vwx31002, ty_Ordering) → new_ltEs14(vwx3002, vwx31002)
new_ltEs14(LT, LT) → True
new_lt5(vwx3000, vwx31000, ty_Bool) → new_lt13(vwx3000, vwx31000)
new_not0True
new_compare32(vwx3000, vwx31000, ty_@0) → new_compare12(vwx3000, vwx31000)
new_esEs8(@0, @0) → True
new_lt6(vwx3001, vwx31001, ty_Int) → new_lt15(vwx3001, vwx31001)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, ty_@0) → new_ltEs8(vwx3000, vwx31000)
new_ltEs18(vwx3002, vwx31002, ty_Bool) → new_ltEs12(vwx3002, vwx31002)
new_min10(vwx8, vwx9, False, dbc) → Just(vwx9)
new_ltEs10(vwx300, vwx3100, ccf) → new_not(new_compare18(vwx300, vwx3100, ccf))
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Bool) → new_ltEs12(vwx3000, vwx31000)
new_esEs22(vwx200, vwx210, ty_Bool) → new_esEs11(vwx200, vwx210)
new_primCmpInt(Pos(Succ(vwx30000)), Neg(vwx31000)) → GT
new_esEs12(vwx20, vwx21, ty_@0) → new_esEs8(vwx20, vwx21)
new_lt5(vwx3000, vwx31000, app(ty_Ratio, dh)) → new_lt11(vwx3000, vwx31000, dh)
new_primMulInt(Pos(vwx30000), Pos(vwx310010)) → Pos(new_primMulNat0(vwx30000, vwx310010))
new_lt9(vwx3000, vwx31000) → new_esEs9(new_compare12(vwx3000, vwx31000))
new_esEs27(vwx200, vwx210, ty_Bool) → new_esEs11(vwx200, vwx210)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, ty_Ordering) → new_ltEs14(vwx3000, vwx31000)
new_esEs12(vwx20, vwx21, ty_Bool) → new_esEs11(vwx20, vwx21)
new_esEs22(vwx200, vwx210, ty_Int) → new_esEs10(vwx200, vwx210)
new_primMulInt(Neg(vwx30000), Neg(vwx310010)) → Pos(new_primMulNat0(vwx30000, vwx310010))
new_lt14(vwx3000, vwx31000) → new_esEs9(new_compare7(vwx3000, vwx31000))
new_esEs16(EQ, EQ) → True
new_esEs20(vwx202, vwx212, ty_Integer) → new_esEs15(vwx202, vwx212)
new_esEs26(vwx200, vwx210, ty_Ordering) → new_esEs16(vwx200, vwx210)
new_primEqNat0(Zero, Succ(vwx2100)) → False
new_primEqNat0(Succ(vwx2000), Zero) → False
new_esEs5(Just(vwx200), Just(vwx210), app(ty_Ratio, cbh)) → new_esEs18(vwx200, vwx210, cbh)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, ty_Integer) → new_ltEs11(vwx3000, vwx31000)
new_esEs27(vwx200, vwx210, ty_Char) → new_esEs14(vwx200, vwx210)
new_esEs26(vwx200, vwx210, app(app(ty_@2, che), chf)) → new_esEs7(vwx200, vwx210, che, chf)
new_ltEs7(Left(vwx3000), Left(vwx31000), app(app(ty_Either, cda), cdb), cch) → new_ltEs7(vwx3000, vwx31000, cda, cdb)
new_compare25(vwx3000, vwx31000, True, db, dc) → EQ
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs12(vwx20, vwx21, ty_Double) → new_esEs19(vwx20, vwx21)
new_esEs27(vwx200, vwx210, app(app(ty_Either, dcd), dce)) → new_esEs4(vwx200, vwx210, dcd, dce)
new_esEs27(vwx200, vwx210, app(app(app(ty_@3, dbd), dbe), dbf)) → new_esEs6(vwx200, vwx210, dbd, dbe, dbf)
new_compare4(:(vwx3000, vwx3001), [], bb) → GT
new_esEs20(vwx202, vwx212, app(ty_[], bde)) → new_esEs17(vwx202, vwx212, bde)
new_compare28(vwx3000, vwx31000, dd) → new_compare210(vwx3000, vwx31000, new_esEs5(vwx3000, vwx31000, dd), dd)
new_esEs22(vwx200, vwx210, app(ty_[], bga)) → new_esEs17(vwx200, vwx210, bga)
new_ltEs18(vwx3002, vwx31002, app(app(ty_@2, gg), gh)) → new_ltEs17(vwx3002, vwx31002, gg, gh)
new_pePe(True, vwx20, vwx21, vwx37, ha) → True
new_esEs26(vwx200, vwx210, app(ty_Maybe, chd)) → new_esEs5(vwx200, vwx210, chd)
new_ltEs20(vwx300, vwx3100, app(ty_Maybe, bc)) → new_ltEs6(vwx300, vwx3100, bc)
new_esEs5(Just(vwx200), Just(vwx210), ty_Double) → new_esEs19(vwx200, vwx210)
new_compare25(vwx3000, vwx31000, False, db, dc) → new_compare15(vwx3000, vwx31000, new_ltEs7(vwx3000, vwx31000, db, dc), db, dc)
new_lt20(vwx3000, vwx31000, ty_@0) → new_lt9(vwx3000, vwx31000)
new_primCmpInt(Neg(Zero), Neg(Succ(vwx310000))) → new_primCmpNat0(Succ(vwx310000), Zero)
new_compare23(vwx3000, vwx31000, True, eb, ec) → EQ
new_primCmpInt(Pos(Zero), Neg(Succ(vwx310000))) → GT
new_esEs11(True, False) → False
new_esEs11(False, True) → False
new_compare110(vwx3000, vwx31000, False, dd) → GT
new_esEs5(Just(vwx200), Just(vwx210), app(app(app(ty_@3, cbd), cbe), cbf)) → new_esEs6(vwx200, vwx210, cbd, cbe, cbf)
new_lt6(vwx3001, vwx31001, ty_Double) → new_lt17(vwx3001, vwx31001)
new_compare4([], :(vwx31000, vwx31001), bb) → LT
new_lt5(vwx3000, vwx31000, ty_Float) → new_lt14(vwx3000, vwx31000)
new_sr0(vwx3000, vwx31001) → new_primMulInt(vwx3000, vwx31001)
new_compare15(vwx3000, vwx31000, False, db, dc) → GT
new_compare32(vwx3000, vwx31000, ty_Int) → new_compare8(vwx3000, vwx31000)
new_compare17(vwx3000, vwx31000) → new_compare27(vwx3000, vwx31000, new_esEs11(vwx3000, vwx31000))
new_esEs20(vwx202, vwx212, app(ty_Ratio, bdf)) → new_esEs18(vwx202, vwx212, bdf)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Double) → new_ltEs15(vwx3000, vwx31000)
new_ltEs19(vwx3001, vwx31001, ty_Ordering) → new_ltEs14(vwx3001, vwx31001)
new_ltEs7(Left(vwx3000), Left(vwx31000), app(ty_[], cdh), cch) → new_ltEs4(vwx3000, vwx31000, cdh)
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Integer, cch) → new_ltEs11(vwx3000, vwx31000)
new_lt6(vwx3001, vwx31001, ty_Float) → new_lt14(vwx3001, vwx31001)
new_ltEs19(vwx3001, vwx31001, ty_Integer) → new_ltEs11(vwx3001, vwx31001)
new_esEs25(vwx201, vwx211, ty_Ordering) → new_esEs16(vwx201, vwx211)
new_lt20(vwx3000, vwx31000, app(ty_[], bbe)) → new_lt16(vwx3000, vwx31000, bbe)
new_esEs21(vwx201, vwx211, ty_Bool) → new_esEs11(vwx201, vwx211)
new_compare32(vwx3000, vwx31000, ty_Bool) → new_compare17(vwx3000, vwx31000)
new_esEs21(vwx201, vwx211, ty_Float) → new_esEs13(vwx201, vwx211)
new_primCmpInt(Neg(Zero), Neg(Zero)) → EQ
new_esEs27(vwx200, vwx210, ty_Float) → new_esEs13(vwx200, vwx210)
new_esEs24(vwx200, vwx210, ty_Int) → new_esEs10(vwx200, vwx210)
new_esEs20(vwx202, vwx212, app(ty_Maybe, bdg)) → new_esEs5(vwx202, vwx212, bdg)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, app(app(ty_Either, cec), ced)) → new_ltEs7(vwx3000, vwx31000, cec, ced)
new_esEs16(LT, LT) → True
new_asAs(False, vwx46) → False
new_esEs18(:%(vwx200, vwx201), :%(vwx210, vwx211), hf) → new_asAs(new_esEs24(vwx200, vwx210, hf), new_esEs23(vwx201, vwx211, hf))
new_lt6(vwx3001, vwx31001, ty_Integer) → new_lt12(vwx3001, vwx31001)
new_ltEs18(vwx3002, vwx31002, ty_Double) → new_ltEs15(vwx3002, vwx31002)
new_primMulInt(Neg(vwx30000), Pos(vwx310010)) → Neg(new_primMulNat0(vwx30000, vwx310010))
new_primMulInt(Pos(vwx30000), Neg(vwx310010)) → Neg(new_primMulNat0(vwx30000, vwx310010))
new_primMulNat0(Succ(vwx300000), Zero) → Zero
new_primMulNat0(Zero, Succ(vwx3100100)) → Zero
new_lt5(vwx3000, vwx31000, app(app(ty_@2, eb), ec)) → new_lt19(vwx3000, vwx31000, eb, ec)
new_compare23(vwx3000, vwx31000, False, eb, ec) → new_compare14(vwx3000, vwx31000, new_ltEs17(vwx3000, vwx31000, eb, ec), eb, ec)
new_esEs22(vwx200, vwx210, ty_Ordering) → new_esEs16(vwx200, vwx210)
new_compare4(:(vwx3000, vwx3001), :(vwx31000, vwx31001), bb) → new_primCompAux0(vwx3000, vwx31000, new_compare4(vwx3001, vwx31001, bb), bb)
new_esEs16(GT, GT) → True
new_ltEs18(vwx3002, vwx31002, app(ty_[], gf)) → new_ltEs4(vwx3002, vwx31002, gf)
new_ltEs19(vwx3001, vwx31001, ty_Char) → new_ltEs16(vwx3001, vwx31001)
new_esEs12(vwx20, vwx21, ty_Char) → new_esEs14(vwx20, vwx21)
new_ltEs14(GT, LT) → False
new_esEs17(:(vwx200, vwx201), :(vwx210, vwx211), he) → new_asAs(new_esEs27(vwx200, vwx210, he), new_esEs17(vwx201, vwx211, he))
new_not(EQ) → new_not0
new_ltEs12(True, True) → True
new_esEs4(Left(vwx200), Left(vwx210), app(ty_Maybe, bhe), bac) → new_esEs5(vwx200, vwx210, bhe)
new_esEs25(vwx201, vwx211, app(ty_[], cfh)) → new_esEs17(vwx201, vwx211, cfh)
new_esEs11(True, True) → True
new_lt5(vwx3000, vwx31000, ty_Double) → new_lt17(vwx3000, vwx31000)
new_esEs25(vwx201, vwx211, app(app(app(ty_@3, cfe), cff), cfg)) → new_esEs6(vwx201, vwx211, cfe, cff, cfg)
new_ltEs12(False, True) → True
new_compare24(vwx3000, vwx31000, False, de, df, dg) → new_compare13(vwx3000, vwx31000, new_ltEs9(vwx3000, vwx31000, de, df, dg), de, df, dg)
new_esEs5(Just(vwx200), Just(vwx210), ty_@0) → new_esEs8(vwx200, vwx210)
new_esEs23(vwx201, vwx211, ty_Integer) → new_esEs15(vwx201, vwx211)
new_compare27(vwx3000, vwx31000, True) → EQ
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, app(app(ty_@2, cfc), cfd)) → new_ltEs17(vwx3000, vwx31000, cfc, cfd)
new_esEs26(vwx200, vwx210, ty_Double) → new_esEs19(vwx200, vwx210)
new_ltEs19(vwx3001, vwx31001, ty_@0) → new_ltEs8(vwx3001, vwx31001)
new_esEs5(Just(vwx200), Nothing, hg) → False
new_esEs5(Nothing, Just(vwx210), hg) → False
new_esEs14(Char(vwx200), Char(vwx210)) → new_primEqNat0(vwx200, vwx210)
new_ltEs6(Nothing, Nothing, bc) → True
new_esEs4(Left(vwx200), Left(vwx210), ty_Float, bac) → new_esEs13(vwx200, vwx210)
new_esEs12(vwx20, vwx21, app(app(app(ty_@3, hb), hc), hd)) → new_esEs6(vwx20, vwx21, hb, hc, hd)
new_ltEs16(vwx300, vwx3100) → new_not(new_compare19(vwx300, vwx3100))
new_esEs5(Just(vwx200), Just(vwx210), ty_Float) → new_esEs13(vwx200, vwx210)
new_esEs4(Left(vwx200), Left(vwx210), app(app(ty_@2, bhf), bhg), bac) → new_esEs7(vwx200, vwx210, bhf, bhg)
new_esEs12(vwx20, vwx21, ty_Int) → new_esEs10(vwx20, vwx21)
new_ltEs20(vwx300, vwx3100, app(app(ty_Either, ccg), cch)) → new_ltEs7(vwx300, vwx3100, ccg, cch)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, app(app(app(ty_@3, cef), ceg), ceh)) → new_ltEs9(vwx3000, vwx31000, cef, ceg, ceh)
new_compare26(vwx3000, vwx31000, False) → new_compare10(vwx3000, vwx31000, new_ltEs14(vwx3000, vwx31000))
new_compare11(vwx3000, vwx31000, False) → GT
new_compare30(vwx3000, vwx31000, de, df, dg) → new_compare24(vwx3000, vwx31000, new_esEs6(vwx3000, vwx31000, de, df, dg), de, df, dg)
new_ltEs14(LT, GT) → True
new_ltEs8(vwx300, vwx3100) → new_not(new_compare12(vwx300, vwx3100))
new_lt20(vwx3000, vwx31000, ty_Integer) → new_lt12(vwx3000, vwx31000)
new_not(LT) → new_not0
new_ltEs14(LT, EQ) → True
new_compare11(vwx3000, vwx31000, True) → LT
new_esEs5(Nothing, Nothing, hg) → True
new_ltEs18(vwx3002, vwx31002, app(ty_Maybe, ga)) → new_ltEs6(vwx3002, vwx31002, ga)
new_compare14(vwx3000, vwx31000, True, eb, ec) → LT
new_esEs4(Left(vwx200), Left(vwx210), ty_Char, bac) → new_esEs14(vwx200, vwx210)
new_compare32(vwx3000, vwx31000, ty_Ordering) → new_compare9(vwx3000, vwx31000)
new_ltEs6(Just(vwx3000), Just(vwx31000), ty_Float) → new_ltEs5(vwx3000, vwx31000)
new_lt6(vwx3001, vwx31001, app(app(ty_Either, ed), ee)) → new_lt7(vwx3001, vwx31001, ed, ee)
new_ltEs19(vwx3001, vwx31001, ty_Double) → new_ltEs15(vwx3001, vwx31001)
new_esEs4(Right(vwx200), Right(vwx210), bab, ty_Double) → new_esEs19(vwx200, vwx210)
new_compare32(vwx3000, vwx31000, ty_Float) → new_compare7(vwx3000, vwx31000)
new_esEs20(vwx202, vwx212, app(app(ty_@2, bdh), bea)) → new_esEs7(vwx202, vwx212, bdh, bea)
new_esEs25(vwx201, vwx211, ty_Double) → new_esEs19(vwx201, vwx211)
new_esEs22(vwx200, vwx210, app(ty_Maybe, bgc)) → new_esEs5(vwx200, vwx210, bgc)
new_lt20(vwx3000, vwx31000, app(ty_Maybe, bah)) → new_lt8(vwx3000, vwx31000, bah)
new_esEs21(vwx201, vwx211, app(ty_Maybe, bfa)) → new_esEs5(vwx201, vwx211, bfa)
new_esEs22(vwx200, vwx210, ty_Integer) → new_esEs15(vwx200, vwx210)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs21(vwx201, vwx211, app(app(app(ty_@3, bed), bee), bef)) → new_esEs6(vwx201, vwx211, bed, bee, bef)
new_compare32(vwx3000, vwx31000, app(app(ty_Either, daa), dab)) → new_compare31(vwx3000, vwx31000, daa, dab)
new_esEs4(Left(vwx200), Left(vwx210), ty_Bool, bac) → new_esEs11(vwx200, vwx210)
new_compare16(Double(vwx3000, vwx3001), Double(vwx31000, vwx31001)) → new_compare8(new_sr0(vwx3000, vwx31000), new_sr0(vwx3001, vwx31001))
new_esEs12(vwx20, vwx21, ty_Ordering) → new_esEs16(vwx20, vwx21)
new_esEs26(vwx200, vwx210, app(app(ty_Either, chg), chh)) → new_esEs4(vwx200, vwx210, chg, chh)
new_asAs(True, vwx46) → vwx46
new_ltEs14(EQ, EQ) → True
new_esEs12(vwx20, vwx21, ty_Integer) → new_esEs15(vwx20, vwx21)
new_lt15(vwx3000, vwx31000) → new_esEs9(new_compare8(vwx3000, vwx31000))
new_primMulNat0(Succ(vwx300000), Succ(vwx3100100)) → new_primPlusNat0(new_primMulNat0(vwx300000, Succ(vwx3100100)), vwx3100100)
new_lt13(vwx3000, vwx31000) → new_esEs9(new_compare17(vwx3000, vwx31000))
new_esEs4(Left(vwx200), Right(vwx210), bab, bac) → False
new_esEs4(Right(vwx200), Left(vwx210), bab, bac) → False
new_esEs5(Just(vwx200), Just(vwx210), app(app(ty_@2, ccb), ccc)) → new_esEs7(vwx200, vwx210, ccb, ccc)
new_esEs27(vwx200, vwx210, ty_Int) → new_esEs10(vwx200, vwx210)
new_esEs21(vwx201, vwx211, ty_Char) → new_esEs14(vwx201, vwx211)
new_esEs23(vwx201, vwx211, ty_Int) → new_esEs10(vwx201, vwx211)
new_esEs21(vwx201, vwx211, ty_Int) → new_esEs10(vwx201, vwx211)
new_esEs4(Left(vwx200), Left(vwx210), app(app(app(ty_@3, bgh), bha), bhb), bac) → new_esEs6(vwx200, vwx210, bgh, bha, bhb)
new_esEs17([], [], he) → True
new_compare32(vwx3000, vwx31000, ty_Integer) → new_compare6(vwx3000, vwx31000)
new_esEs17(:(vwx200, vwx201), [], he) → False
new_esEs17([], :(vwx210, vwx211), he) → False
new_esEs27(vwx200, vwx210, ty_@0) → new_esEs8(vwx200, vwx210)
new_esEs4(Right(vwx200), Right(vwx210), bab, ty_Float) → new_esEs13(vwx200, vwx210)
new_esEs13(Float(vwx200, vwx201), Float(vwx210, vwx211)) → new_esEs10(new_sr0(vwx200, vwx210), new_sr0(vwx201, vwx211))
new_lt10(vwx3000, vwx31000, de, df, dg) → new_esEs9(new_compare30(vwx3000, vwx31000, de, df, dg))
new_esEs4(Left(vwx200), Left(vwx210), ty_@0, bac) → new_esEs8(vwx200, vwx210)
new_compare10(vwx3000, vwx31000, True) → LT
new_lt5(vwx3000, vwx31000, ty_Char) → new_lt18(vwx3000, vwx31000)
new_ltEs7(Right(vwx3000), Right(vwx31000), ccg, app(ty_Maybe, cee)) → new_ltEs6(vwx3000, vwx31000, cee)
new_compare32(vwx3000, vwx31000, app(ty_Ratio, dag)) → new_compare18(vwx3000, vwx31000, dag)
new_ltEs4(vwx300, vwx3100, bb) → new_not(new_compare4(vwx300, vwx3100, bb))
new_compare13(vwx3000, vwx31000, True, de, df, dg) → LT
new_compare10(vwx3000, vwx31000, False) → GT
new_esEs10(vwx20, vwx21) → new_primEqInt(vwx20, vwx21)
new_lt5(vwx3000, vwx31000, app(ty_Maybe, dd)) → new_lt8(vwx3000, vwx31000, dd)
new_primCompAux00(vwx51, GT) → GT
new_esEs5(Just(vwx200), Just(vwx210), app(app(ty_Either, ccd), cce)) → new_esEs4(vwx200, vwx210, ccd, cce)
new_primCmpInt(Pos(Zero), Pos(Zero)) → EQ
new_compare18(:%(vwx3000, vwx3001), :%(vwx31000, vwx31001), ty_Int) → new_compare8(new_sr0(vwx3000, vwx31001), new_sr0(vwx31000, vwx3001))
new_ltEs14(EQ, GT) → True
new_esEs12(vwx20, vwx21, app(ty_Maybe, hg)) → new_esEs5(vwx20, vwx21, hg)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs27(vwx200, vwx210, ty_Integer) → new_esEs15(vwx200, vwx210)
new_esEs21(vwx201, vwx211, app(ty_Ratio, beh)) → new_esEs18(vwx201, vwx211, beh)
new_esEs4(Left(vwx200), Left(vwx210), app(ty_Ratio, bhd), bac) → new_esEs18(vwx200, vwx210, bhd)
new_primCmpInt(Neg(Succ(vwx30000)), Pos(vwx31000)) → LT
new_ltEs7(Left(vwx3000), Left(vwx31000), ty_Bool, cch) → new_ltEs12(vwx3000, vwx31000)
new_esEs27(vwx200, vwx210, ty_Double) → new_esEs19(vwx200, vwx210)

The set Q consists of the following terms:

new_lt19(x0, x1, x2, x3)
new_primCmpInt(Neg(Zero), Pos(Succ(x0)))
new_primCmpInt(Pos(Zero), Neg(Succ(x0)))
new_ltEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_ltEs18(x0, x1, app(ty_[], x2))
new_ltEs18(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Double)
new_lt6(x0, x1, ty_Ordering)
new_ltEs20(x0, x1, ty_Float)
new_esEs4(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(True, True)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(Left(x0), Left(x1), app(ty_[], x2), x3)
new_ltEs19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(Right(x0), Right(x1), x2, ty_Bool)
new_compare15(x0, x1, False, x2, x3)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_ltEs5(x0, x1)
new_primCmpNat0(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Integer)
new_esEs12(x0, x1, ty_Integer)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_lt11(x0, x1, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_compare4(:(x0, x1), [], x2)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs14(Char(x0), Char(x1))
new_esEs5(Nothing, Nothing, x0)
new_compare8(x0, x1)
new_ltEs9(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_compare7(Float(x0, x1), Float(x2, x3))
new_esEs4(Right(x0), Right(x1), x2, ty_Double)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_lt6(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs7(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs9(EQ)
new_compare32(x0, x1, ty_Integer)
new_esEs10(x0, x1)
new_esEs21(x0, x1, ty_Int)
new_compare32(x0, x1, ty_Int)
new_compare32(x0, x1, ty_Char)
new_esEs21(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_compare30(x0, x1, x2, x3, x4)
new_esEs22(x0, x1, ty_@0)
new_compare32(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs7(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_ltEs7(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_lt6(x0, x1, app(ty_Maybe, x2))
new_esEs11(False, True)
new_esEs11(True, False)
new_esEs26(x0, x1, ty_@0)
new_ltEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs5(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_lt20(x0, x1, ty_Float)
new_primMulInt(Pos(x0), Neg(x1))
new_primMulInt(Neg(x0), Pos(x1))
new_compare19(Char(x0), Char(x1))
new_esEs8(@0, @0)
new_esEs16(GT, LT)
new_esEs16(LT, GT)
new_primEqNat0(Zero, Succ(x0))
new_ltEs6(Just(x0), Just(x1), ty_Float)
new_esEs27(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Double)
new_ltEs6(Just(x0), Just(x1), ty_Integer)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_lt4(x0, x1)
new_min10(x0, x1, False, x2)
new_compare9(x0, x1)
new_lt5(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt5(x0, x1, ty_Ordering)
new_esEs4(Right(x0), Right(x1), x2, ty_Ordering)
new_lt18(x0, x1)
new_ltEs19(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Int)
new_primCmpInt(Neg(Succ(x0)), Neg(x1))
new_lt6(x0, x1, ty_Float)
new_lt5(x0, x1, app(ty_[], x2))
new_esEs17([], [], x0)
new_compare16(Double(x0, x1), Double(x2, x3))
new_esEs4(Right(x0), Right(x1), x2, ty_Float)
new_esEs4(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_compare32(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs18(x0, x1, ty_Float)
new_ltEs6(Just(x0), Just(x1), ty_Int)
new_esEs26(x0, x1, app(ty_[], x2))
new_ltEs18(x0, x1, app(ty_Maybe, x2))
new_primMulInt(Neg(x0), Neg(x1))
new_primMulNat0(Succ(x0), Zero)
new_ltEs7(Left(x0), Left(x1), ty_Float, x2)
new_ltEs18(x0, x1, ty_Char)
new_esEs22(x0, x1, ty_Bool)
new_lt20(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs4(x0, x1, x2)
new_lt20(x0, x1, ty_Double)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs14(EQ, EQ)
new_primEqNat0(Zero, Zero)
new_ltEs6(Just(x0), Nothing, x1)
new_ltEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_lt20(x0, x1, app(ty_[], x2))
new_lt6(x0, x1, ty_Bool)
new_ltEs10(x0, x1, x2)
new_ltEs16(x0, x1)
new_esEs12(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_compare31(x0, x1, x2, x3)
new_ltEs6(Just(x0), Just(x1), ty_Double)
new_ltEs7(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_compare12(@0, @0)
new_esEs5(Just(x0), Just(x1), ty_Ordering)
new_ltEs19(x0, x1, ty_Char)
new_ltEs20(x0, x1, app(app(ty_Either, x2), x3))
new_primCompAux00(x0, GT)
new_esEs12(x0, x1, app(app(ty_Either, x2), x3))
new_compare11(x0, x1, True)
new_esEs4(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_ltEs19(x0, x1, app(ty_Maybe, x2))
new_primMulNat0(Zero, Zero)
new_ltEs7(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_ltEs6(Just(x0), Just(x1), ty_@0)
new_esEs6(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_sr(Integer(x0), Integer(x1))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_lt6(x0, x1, ty_Int)
new_esEs5(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs5(Just(x0), Just(x1), ty_Double)
new_esEs4(Right(x0), Right(x1), x2, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs20(x0, x1, ty_@0)
new_esEs12(x0, x1, app(ty_Maybe, x2))
new_ltEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_ltEs20(x0, x1, ty_Bool)
new_esEs4(Right(x0), Right(x1), x2, ty_@0)
new_compare23(x0, x1, True, x2, x3)
new_esEs12(x0, x1, ty_Char)
new_compare210(x0, x1, True, x2)
new_esEs16(GT, GT)
new_esEs21(x0, x1, ty_Integer)
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_ltEs7(Left(x0), Left(x1), ty_Ordering, x2)
new_compare28(x0, x1, x2)
new_compare18(:%(x0, x1), :%(x2, x3), ty_Int)
new_ltEs7(Left(x0), Left(x1), ty_Int, x2)
new_lt5(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs18(x0, x1, app(ty_Ratio, x2))
new_ltEs18(x0, x1, ty_Ordering)
new_esEs5(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs13(Float(x0, x1), Float(x2, x3))
new_esEs5(Just(x0), Just(x1), ty_Integer)
new_primEqNat0(Succ(x0), Zero)
new_primCmpInt(Neg(Succ(x0)), Pos(x1))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_compare32(x0, x1, app(ty_[], x2))
new_primCmpInt(Pos(Succ(x0)), Neg(x1))
new_compare4(:(x0, x1), :(x2, x3), x4)
new_compare110(x0, x1, True, x2)
new_esEs20(x0, x1, ty_Char)
new_ltEs19(x0, x1, app(ty_Ratio, x2))
new_lt8(x0, x1, x2)
new_lt9(x0, x1)
new_asAs(False, x0)
new_compare23(x0, x1, False, x2, x3)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_lt5(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Int)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(False, False)
new_ltEs12(False, False)
new_esEs5(Nothing, Just(x0), x1)
new_min1(Just(x0), Just(x1), x2)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Float)
new_ltEs7(Right(x0), Right(x1), x2, ty_@0)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_primMulInt(Pos(x0), Pos(x1))
new_ltEs7(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_compare4([], [], x0)
new_esEs22(x0, x1, ty_Char)
new_ltEs7(Right(x0), Right(x1), x2, ty_Ordering)
new_ltEs20(x0, x1, app(ty_Ratio, x2))
new_ltEs19(x0, x1, ty_Bool)
new_esEs5(Just(x0), Nothing, x1)
new_esEs27(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Double)
new_primMulNat0(Zero, Succ(x0))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Char)
new_compare13(x0, x1, False, x2, x3, x4)
new_esEs4(Left(x0), Left(x1), ty_Double, x2)
new_esEs25(x0, x1, ty_Int)
new_primPlusNat1(Zero, Zero)
new_ltEs7(Right(x0), Right(x1), x2, ty_Bool)
new_not0
new_ltEs7(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs4(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_lt20(x0, x1, ty_Int)
new_compare6(Integer(x0), Integer(x1))
new_ltEs7(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs8(x0, x1)
new_esEs9(GT)
new_ltEs14(LT, LT)
new_esEs27(x0, x1, ty_@0)
new_ltEs20(x0, x1, ty_@0)
new_lt14(x0, x1)
new_primCmpInt(Neg(Zero), Neg(Zero))
new_esEs25(x0, x1, ty_@0)
new_primCompAux00(x0, LT)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Ordering)
new_ltEs6(Nothing, Nothing, x0)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_min1(Just(x0), Nothing, x1)
new_esEs26(x0, x1, ty_Integer)
new_ltEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt5(x0, x1, app(ty_Ratio, x2))
new_esEs5(Just(x0), Just(x1), ty_@0)
new_lt13(x0, x1)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_compare32(x0, x1, app(app(ty_@2, x2), x3))
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs4(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_lt6(x0, x1, ty_Char)
new_primCmpNat0(Zero, Succ(x0))
new_pePe(True, x0, x1, x2, x3)
new_esEs26(x0, x1, ty_Double)
new_compare32(x0, x1, ty_Ordering)
new_not(GT)
new_esEs12(x0, x1, app(ty_Ratio, x2))
new_ltEs7(Left(x0), Left(x1), ty_Bool, x2)
new_ltEs7(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Bool)
new_ltEs6(Nothing, Just(x0), x1)
new_compare17(x0, x1)
new_compare15(x0, x1, True, x2, x3)
new_esEs20(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_ltEs7(Right(x0), Left(x1), x2, x3)
new_ltEs7(Left(x0), Right(x1), x2, x3)
new_lt20(x0, x1, app(ty_Maybe, x2))
new_lt20(x0, x1, ty_Ordering)
new_ltEs14(LT, EQ)
new_ltEs14(EQ, LT)
new_esEs12(x0, x1, app(app(ty_@2, x2), x3))
new_compare32(x0, x1, app(ty_Ratio, x2))
new_lt6(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(Left(x0), Right(x1), x2, x3)
new_esEs4(Right(x0), Left(x1), x2, x3)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_lt5(x0, x1, ty_@0)
new_lt20(x0, x1, app(ty_Ratio, x2))
new_compare32(x0, x1, ty_Bool)
new_esEs4(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_compare27(x0, x1, False)
new_ltEs20(x0, x1, ty_Ordering)
new_lt5(x0, x1, ty_Char)
new_primCmpInt(Pos(Zero), Pos(Zero))
new_esEs4(Left(x0), Left(x1), ty_Int, x2)
new_lt20(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs19(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Zero))
new_min1(Nothing, Just(x0), x1)
new_ltEs7(Left(x0), Left(x1), ty_Double, x2)
new_compare25(x0, x1, False, x2, x3)
new_ltEs7(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs27(x0, x1, ty_Float)
new_esEs4(Left(x0), Left(x1), ty_Char, x2)
new_esEs26(x0, x1, ty_Ordering)
new_ltEs7(Left(x0), Left(x1), ty_@0, x2)
new_lt20(x0, x1, app(app(ty_Either, x2), x3))
new_min1(Nothing, Nothing, x0)
new_ltEs7(Left(x0), Left(x1), ty_Char, x2)
new_ltEs18(x0, x1, ty_@0)
new_compare110(x0, x1, False, x2)
new_esEs16(LT, LT)
new_ltEs20(x0, x1, ty_Char)
new_lt5(x0, x1, ty_Float)
new_ltEs18(x0, x1, ty_Double)
new_compare32(x0, x1, ty_@0)
new_esEs5(Just(x0), Just(x1), app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs25(x0, x1, ty_Ordering)
new_esEs4(Left(x0), Left(x1), ty_@0, x2)
new_lt6(x0, x1, ty_Integer)
new_esEs19(Double(x0, x1), Double(x2, x3))
new_ltEs20(x0, x1, app(ty_[], x2))
new_esEs4(Right(x0), Right(x1), x2, ty_Integer)
new_lt12(x0, x1)
new_esEs12(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(x0, x1, ty_Int)
new_lt20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs7(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, ty_@0)
new_esEs4(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_compare14(x0, x1, False, x2, x3)
new_ltEs19(x0, x1, ty_Float)
new_esEs5(Just(x0), Just(x1), ty_Int)
new_ltEs7(Right(x0), Right(x1), x2, ty_Int)
new_compare26(x0, x1, False)
new_esEs27(x0, x1, ty_Int)
new_esEs15(Integer(x0), Integer(x1))
new_primPlusNat0(Zero, x0)
new_esEs9(LT)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_ltEs7(Right(x0), Right(x1), x2, ty_Integer)
new_lt16(x0, x1, x2)
new_esEs20(x0, x1, app(ty_[], x2))
new_compare27(x0, x1, True)
new_ltEs12(True, False)
new_ltEs12(False, True)
new_esEs24(x0, x1, ty_Integer)
new_lt20(x0, x1, ty_@0)
new_esEs20(x0, x1, ty_Float)
new_ltEs17(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs21(x0, x1, ty_Double)
new_ltEs20(x0, x1, app(ty_Maybe, x2))
new_ltEs14(EQ, GT)
new_ltEs14(GT, EQ)
new_primCmpNat0(Zero, Zero)
new_compare11(x0, x1, False)
new_lt20(x0, x1, ty_Bool)
new_min10(x0, x1, True, x2)
new_ltEs15(x0, x1)
new_esEs7(@2(x0, x1), @2(x2, x3), x4, x5)
new_ltEs20(x0, x1, ty_Integer)
new_esEs12(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Char)
new_ltEs7(Left(x0), Left(x1), ty_Integer, x2)
new_esEs5(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Int)
new_ltEs7(Right(x0), Right(x1), x2, ty_Char)
new_ltEs7(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_ltEs20(x0, x1, ty_Double)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_ltEs20(x0, x1, ty_Int)
new_primMulNat0(Succ(x0), Succ(x1))
new_primCompAux0(x0, x1, x2, x3)
new_esEs4(Right(x0), Right(x1), x2, app(ty_[], x3))
new_lt10(x0, x1, x2, x3, x4)
new_esEs12(x0, x1, ty_Ordering)
new_ltEs14(LT, GT)
new_ltEs14(GT, LT)
new_compare13(x0, x1, True, x2, x3, x4)
new_ltEs18(x0, x1, ty_Integer)
new_primCmpInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Ordering)
new_compare26(x0, x1, True)
new_ltEs6(Just(x0), Just(x1), ty_Char)
new_primCmpInt(Pos(Succ(x0)), Pos(x1))
new_esEs26(x0, x1, ty_Bool)
new_ltEs7(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs22(x0, x1, ty_Float)
new_esEs5(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_compare24(x0, x1, False, x2, x3, x4)
new_ltEs14(GT, GT)
new_ltEs18(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Float)
new_ltEs19(x0, x1, ty_@0)
new_esEs12(x0, x1, ty_@0)
new_esEs4(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_compare25(x0, x1, True, x2, x3)
new_esEs5(Just(x0), Just(x1), ty_Bool)
new_esEs12(x0, x1, ty_Double)
new_not(EQ)
new_lt6(x0, x1, ty_Double)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(LT, EQ)
new_esEs16(EQ, LT)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs16(EQ, EQ)
new_primCmpInt(Neg(Zero), Pos(Zero))
new_primCmpInt(Pos(Zero), Neg(Zero))
new_ltEs19(x0, x1, ty_Integer)
new_compare10(x0, x1, True)
new_lt6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs18(x0, x1, ty_Int)
new_compare10(x0, x1, False)
new_primPlusNat1(Succ(x0), Zero)
new_esEs27(x0, x1, ty_Integer)
new_esEs4(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_ltEs6(Just(x0), Just(x1), ty_Bool)
new_ltEs12(True, True)
new_lt15(x0, x1)
new_esEs4(Left(x0), Left(x1), ty_Bool, x2)
new_lt5(x0, x1, ty_Int)
new_esEs4(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs25(x0, x1, ty_Bool)
new_ltEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_lt5(x0, x1, ty_Bool)
new_compare29(x0, x1, x2, x3)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_primCmpInt(Pos(Zero), Pos(Succ(x0)))
new_compare14(x0, x1, True, x2, x3)
new_lt7(x0, x1, x2, x3)
new_esEs27(x0, x1, ty_Double)
new_lt6(x0, x1, app(ty_[], x2))
new_esEs16(GT, EQ)
new_esEs16(EQ, GT)
new_lt20(x0, x1, ty_Integer)
new_lt6(x0, x1, ty_@0)
new_lt5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs6(Just(x0), Just(x1), app(ty_[], x2))
new_compare32(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_Int)
new_esEs5(Just(x0), Just(x1), ty_Char)
new_esEs12(x0, x1, ty_Float)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs4(Right(x0), Right(x1), x2, ty_Int)
new_lt6(x0, x1, app(ty_Ratio, x2))
new_lt17(x0, x1)
new_esEs26(x0, x1, ty_Float)
new_ltEs19(x0, x1, app(ty_[], x2))
new_compare24(x0, x1, True, x2, x3, x4)
new_esEs17(:(x0, x1), [], x2)
new_ltEs19(x0, x1, ty_Int)
new_esEs4(Left(x0), Left(x1), ty_Float, x2)
new_esEs4(Left(x0), Left(x1), ty_Ordering, x2)
new_primCompAux00(x0, EQ)
new_ltEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Ordering)
new_compare32(x0, x1, app(ty_Maybe, x2))
new_compare210(x0, x1, False, x2)
new_esEs20(x0, x1, ty_Int)
new_ltEs11(x0, x1)
new_esEs21(x0, x1, ty_Ordering)
new_primPlusNat0(Succ(x0), x1)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs5(Just(x0), Just(x1), app(ty_Maybe, x2))
new_sr0(x0, x1)
new_esEs20(x0, x1, ty_Bool)
new_compare4([], :(x0, x1), x2)
new_compare32(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_esEs25(x0, x1, ty_Char)
new_pePe(False, x0, x1, x2, x3)
new_ltEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primCmpNat0(Succ(x0), Succ(x1))
new_ltEs13(x0, x1)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_lt5(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_Integer)
new_ltEs7(Right(x0), Right(x1), x2, ty_Double)
new_not(LT)
new_compare18(:%(x0, x1), :%(x2, x3), ty_Integer)
new_lt5(x0, x1, app(ty_Maybe, x2))
new_ltEs18(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, app(ty_Maybe, x2))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: